allaun
3b1e590b09
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>
1.8 KiB
Deletion Log — 2026-07-03
formal/CoreFormalism/SidonWrapping.lean
Action: deleted from the active tree; full 81-line source preserved at
archive/2026-07-03/formal/CoreFormalism/SidonWrapping.lean.
Why deleted (rotted orphan):
- Unregistered — not listed in any
lakefile, so never in the build tree. - Imported nowhere — the only mention across the repo was a stale line in
docs/review_findings.md(which wrongly called it "registered"); no.leanimports it. - Two unjustified
sorry(lines 58, 60) with no CITED/CONJECTURE/JUSTIFICATION /HONESTY CLASS tag in range — the sole failing findings of the strict anti-smuggle CI (scripts/anti_smuggle_check.py --ci formal). crtLiftarity mismatch — declaredaxiom crtLift (r₁ r₂ : ℤ) : ℤ(2 args) but called with 4 args instrandLift(crtLift L₁ L₂ …); would not typecheck if ever registered.
Provenance of the decision: flagged in the prior session as the "sole
remaining --ci blocker," left pending a delete/quarantine/fix choice. On
2026-07-03 the anti-smuggle scanner was hardened (standalone-sorry detection
added; the by\n sorry shape had previously evaded the := sorry-only regex),
which turned an incorrectly-green CI red on exactly these two sorries. User chose
delete + archive.
Recovery: the preserved copy is complete and self-describing. To revive, the
real work needed is: fix crtLift to the correct CRT signature (or use
Mathlib/Data/ZMod CRT directly), discharge both sorrys, tag honesty class,
and register in the lakefile. It was HONESTY CLASS: DEVELOPMENT scaffold — the
2-modulus Sidon "wrapping criterion" (image sums differ by (wrap₁−wrap₂)·M).
Post-deletion state: scripts/anti_smuggle_check.py --ci formal → PASS
(exit 0), no vacuities, all custom axioms justified.