allaun 3b1e590b09 chore(anti-smuggle): patch stealth-True + bare-sorry blind spots; archive SidonWrapping orphan ... 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>		2026-07-03 15:07:49 -05:00
..
2026-07-02	Archive rydberg_braid_cross_domain_scan.md	2026-07-02 03:44:36 +02:00
2026-07-03	chore(anti-smuggle): patch stealth-True + bare-sorry blind spots; archive SidonWrapping orphan	2026-07-03 15:07:49 -05:00