mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-19 04:00:34 +00:00
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>
34 lines
1.8 KiB
Markdown
34 lines
1.8 KiB
Markdown
# 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 `.lean`
|
||
imports 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`).
|
||
- **`crtLift` arity mismatch** — declared `axiom crtLift (r₁ r₂ : ℤ) : ℤ` (2 args)
|
||
but called with 4 args in `strandLift` (`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 `sorry`s, 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.
|