Scanner (scripts/anti_smuggle_check.py):
- detect trivially-inhabited Prop defs — Nonempty (M→M), True, Nonempty Unit —
the stealth-True pattern that evaded the `:= True`-only check; leaves real
predicates like Nonempty (KählerManifold V) untouched.
- flag standalone `sorry` (the `by\n sorry` shape) that evaded the
`:=`/`=>`-prefixed EMPTY_SORRY regex; routed through the same
justification-tag window so tagged research sorries stay clean.
Archive:
- preserve + log formal/CoreFormalism/SidonWrapping.lean, a rotted orphan
(never registered, imported nowhere, crtLift arity mismatch, 2 unjustified
sorries). File was untracked, so removed from disk directly; full source +
rationale kept under archive/2026-07-03/ with DELETION_LOG.md.
Effect: strict `anti_smuggle_check.py --ci formal` was a false green (missed the
two gaps above); now an honest green after the orphan removal.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
