From 3b1e590b09afceb53d458f14601b5288fb4c18e0 Mon Sep 17 00:00:00 2001 From: allaun Date: Fri, 3 Jul 2026 15:07:49 -0500 Subject: [PATCH] chore(anti-smuggle): patch stealth-True + bare-sorry blind spots; archive SidonWrapping orphan MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- archive/2026-07-03/DELETION_LOG.md | 34 ++++++++ .../formal/CoreFormalism/SidonWrapping.lean | 81 +++++++++++++++++++ scripts/anti_smuggle_check.py | 54 ++++++++++++- 3 files changed, 166 insertions(+), 3 deletions(-) create mode 100644 archive/2026-07-03/DELETION_LOG.md create mode 100644 archive/2026-07-03/formal/CoreFormalism/SidonWrapping.lean diff --git a/archive/2026-07-03/DELETION_LOG.md b/archive/2026-07-03/DELETION_LOG.md new file mode 100644 index 00000000..97e3ebca --- /dev/null +++ b/archive/2026-07-03/DELETION_LOG.md @@ -0,0 +1,34 @@ +# 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. diff --git a/archive/2026-07-03/formal/CoreFormalism/SidonWrapping.lean b/archive/2026-07-03/formal/CoreFormalism/SidonWrapping.lean new file mode 100644 index 00000000..6a39cf95 --- /dev/null +++ b/archive/2026-07-03/formal/CoreFormalism/SidonWrapping.lean @@ -0,0 +1,81 @@ +import Mathlib.Data.Nat.Basic +import Mathlib.Data.Int.Basic +import Mathlib.Tactic + +open Nat + +/-! +# Sidon Creation: Wrapping Criterion + +STATUS: DEVELOPMENT — NOT part of active build. +HONESTY CLASS: DEVELOPMENT (in progress, contains untagged sorries and axioms) + +Two pairs (a,b) and (c,d) with a+b = c+d = T collide under F modulo M, +but their integer lifts ℤ may differ if the individual sums straddle the +modulus boundary M differently. This breaks the Sidon collision. + +## Theorem (Wrapping Criterion) + +Let F̂(a) ∈ [0, M) be the CRT integer lift of a. +If a+b = c+d but (F̂(a)+F̂(b) ≥ M) ≠ (F̂(c)+F̂(d) ≥ M), +then F(A) is Sidon where A was not. + +## 2-modulus special case + +For k = 2 with moduli (L₁, L₂), the CRT lift has closed form: + F̂(a) = a + L₁·((S − 2a) · L₁⁻¹ mod L₂) +where L₁⁻¹ is the modular inverse of L₁ modulo L₂. +-/ + +variable (L₁ L₂ S : ℕ) + +/-- CRT inverse: given residues (r₁ mod L₁, r₂ mod L₂), return the unique +integer in [0, L₁·L₂) with those residues. Requires gcd(L₁, L₂) = 1. This +is left as an axiom for now; the full CRT lemma is in Mathlib/Data/ZMod. +HONESTY CLASS: DEVELOPMENT (scaffold axiom, not used in active build). -/ +axiom crtLift (r₁ r₂ : ℤ) : ℤ + +/-- The CRT lift of the strand pair (a mod L₁, S−a mod L₂). -/ +def strandLift (a : ℤ) : ℤ := + crtLift L₁ L₂ (a % (L₁ : ℤ)) (((S : ℤ) - a) % (L₂ : ℤ)) + +/-- Wrapping indicator: 1 if the sum of two lifts crosses M = L₁·L₂, else 0. -/ +def wrap (a b : ℤ) : ℕ := + if strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≥ (L₁ : ℕ) * L₂ then 1 else 0 + +/-- +Two pairs (a,b) and (c,d) with the same integer sum T = a+b = c+d. +Their image sums differ by exactly(wrap₁ − wrap₂)·M. +-/ +theorem wrapping_diff (a b c d : ℤ) (hsum : a + b = c + d) : + (strandLift L₁ L₂ S a + strandLift L₁ L₂ S b) - + (strandLift L₁ L₂ S c + strandLift L₁ L₂ S d) = + ((wrap L₁ L₂ S a b : ℤ) - (wrap L₁ L₂ S c d : ℤ)) * ((L₁ : ℕ) * L₂ : ℤ) := by + have hmod : strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≡ + strandLift L₁ L₂ S c + strandLift L₁ L₂ S d [ZMOD (L₁ : ℕ) * L₂] := by + -- Both sums are ≡ T (mod L₁) and ≡ 2S−T (mod L₂), hence ≡ T (mod M) by CRT + -- (This holds by AXIOM because crtLift is a CRT representative) + sorry + -- The difference is a multiple of M, either 0 or ±M depending on wraps + sorry + +/-- +Sidon creation: if the two pairs wrap differently, their integer sums differ. +-/ +theorem sidon_creation (a b c d : ℤ) (hsum : a + b = c + d) + (hw : wrap L₁ L₂ S a b ≠ wrap L₁ L₂ S c d) : + strandLift L₁ L₂ S a + strandLift L₁ L₂ S b ≠ + strandLift L₁ L₂ S c + strandLift L₁ L₂ S d := by + intro heq + have := wrapping_diff L₁ L₂ S a b c d hsum + have hzero : (wrap L₁ L₂ S a b : ℤ) - (wrap L₁ L₂ S c d : ℤ) = 0 := by + nlinarith + have : wrap L₁ L₂ S a b = wrap L₁ L₂ S c d := by + omega + exact hw this + +-- #eval witness for the Sidon example +#eval let L₁ := 3; L₂ := 4; S := 7 in + wrap L₁ L₂ S (1 : ℤ) (6 : ℤ) -- expected: 1 (10+9=19 ≥ 12) +#eval let L₁ := 3; L₂ := 4; S := 7 in + wrap L₁ L₂ S (2 : ℤ) (5 : ℤ) -- expected: 0 (5+2=7 < 12) diff --git a/scripts/anti_smuggle_check.py b/scripts/anti_smuggle_check.py index 175ee0fe..88eeb889 100644 --- a/scripts/anti_smuggle_check.py +++ b/scripts/anti_smuggle_check.py @@ -44,6 +44,11 @@ LAMBDA_RFL = re.compile( r'^\s*:=\s*(fun\s+(\w+\s+)+\w+\s*=>\s*rfl|λ\s+(\w+\s+)+\w+\s*=>\s*rfl)\s*$' ) EMPTY_SORRY = re.compile(r'^\s*(:=|=>)\s*(by\s+)?sorry\s*$') +# Standalone `sorry` / `by sorry` at the start of a line (the `by\n sorry` +# shape) — evades EMPTY_SORRY, which needs a `:=`/`=>` prefix. Trailing comment +# allowed (`\b`, not `$`), so `sorry -- CONJECTURE: …` still matches and is +# then cleared by the justification-window check. +STANDALONE_SORRY = re.compile(r'^\s*(by\s+)?sorry\b') # Axiom declarations — any custom axiom must carry a justification tag AXIOM_DECL = re.compile(r'^\s*axiom\s+(\w+)\b') @@ -52,6 +57,39 @@ AXIOM_JUSTIFIED = re.compile( re.IGNORECASE ) +# Predicate defs whose body is TRIVIALLY INHABITED — "stealth True". +# A `def NAME ... : Prop := ` where is closable with no real +# content lets a companion `theorem NAME ... := ⟨id⟩ / trivial` vacuously +# "prove" a named conjecture while dodging the `:= True` scanner (the body is +# not literally True). The canonical trap is `Nonempty (M → M)` — inhabited by +# `⟨id⟩`. Detect the concrete, defensible set; a real predicate like +# `Nonempty (KählerManifold V)` (structure argument, no self-arrow) is NOT hit. +DEF_PROP = re.compile( + r'def\s+(\w+)\b.*?:\s*Prop\s*:=\s*(.+?)\s*$', re.MULTILINE +) +# Nonempty (X → X): identity inhabits it. Domain must equal codomain. +NONEMPTY_ENDO = re.compile(r'^Nonempty\s*\(\s*([\w.]+)\s*(?:→|->)\s*([\w.]+)\s*\)$') +# Directly trivially-inhabited bodies (Prop-level units / reflexive True). +TRIVIAL_BODY = re.compile( + r'^(True' + r'|Nonempty\s+(?:PUnit|Unit|True)\b.*' + r'|Nonempty\s*\(\s*(?:PUnit|Unit|True)\b.*\)' + r'|PUnit|Unit)$' +) + + +def is_trivially_inhabited_body(body: str) -> bool: + """True if a `: Prop :=` body is closable with no mathematical content.""" + b = body.strip().rstrip('-').strip() # drop trailing `-- comment` start + # strip a trailing inline comment if present + b = re.split(r'\s--', b, maxsplit=1)[0].strip() + if TRIVIAL_BODY.match(b): + return True + m = NONEMPTY_ENDO.match(b) + if m and m.group(1) == m.group(2): + return True + return False + def check_file(path: str, ci_mode: bool) -> int: """Check a single .lean file for smuggle patterns. Returns finding count.""" @@ -112,12 +150,12 @@ def check_file(path: str, ci_mode: bool) -> int: findings += 1 print(f" [SMUGGLE] {rel}:{i + 1} `fun ... => rfl` lambda as theorem body") - if EMPTY_SORRY.match(stripped) and ci_mode: + if (EMPTY_SORRY.match(stripped) or STANDALONE_SORRY.match(stripped)) and ci_mode: # Check if the sorry is justified (has CITED/CONJECTURE/JUSTIFICATION tag nearby) - surrounding = '\n'.join(lines[max(0, i - 5):min(len(lines), i + 2)]) + surrounding = '\n'.join(lines[max(0, i - 8):min(len(lines), i + 2)]) if not AXIOM_JUSTIFIED.search(surrounding): findings += 1 - print(f" [WARN] {rel}:{i + 1} bare sorry without justification tag " + print(f" [SMUGGLE] {rel}:{i + 1} bare sorry without justification tag " f"(expected CITED/CONJECTURE/JUSTIFICATION)") # Check for vacuous-predicate proofs: `:= trivial` or `:= by trivial` @@ -170,6 +208,16 @@ def check_file(path: str, ci_mode: bool) -> int: f"WITHOUT justification tag " f"(expected CITED/CONJECTURE/JUSTIFICATION in docstring)") + # 6. Stealth-True predicate defs: `def NAME ... : Prop := `. + # Catches the `Nonempty (M → M)` blind spot that the `:= True` scanner misses. + for m in DEF_PROP.finditer(content): + name, body = m.group(1), m.group(2) + if is_trivially_inhabited_body(body): + findings += 1 + print(f" [SMUGGLE] {rel}:{line_of(content, m.start())} def '{name}' " + f"is a stealth-True predicate (body '{body.strip()}' is trivially " + f"inhabited — use an opaque `axiom` signature instead)") + return findings