diff --git a/docs/reviews/avmisa_audit_report.md b/docs/reviews/avmisa_audit_report.md new file mode 100644 index 00000000..4df7e133 --- /dev/null +++ b/docs/reviews/avmisa_audit_report.md @@ -0,0 +1,218 @@ +# AVMIsa Manual Math Audit — Vulnerability Report + +This report walks through every arithmetic path in the AVM ISA step-by-step, +identifies how each can go wrong, and proposes concrete mitigations. + +--- + +## Source Files Under Audit + +| File | Role | +|------|------| +| [FixedPoint.lean](file:///home/allaun/SilverSight/Core/SilverSight/FixedPoint.lean) | Q16_16 type definition + arithmetic kernels | +| [Step.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Step.lean) | AVM instruction semantics | +| [State.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/State.lean) | Machine state (stack, locals, pc) | +| [Run.lean](file:///home/allaun/SilverSight/formal/SilverSight/AVMIsa/Run.lean) | Fuel-bounded execution loop | + +--- + +## §1 — Arithmetic Vulnerability Surfaces + +### V1. Multiplication Intermediate Overflow ⚠️ CRITICAL + +**Definition:** +```lean +def mul (a b : Q16_16) : Q16_16 := ofRawInt ((a.toInt * b.toInt) / q16Scale) +``` + +**The problem:** `a.toInt` and `b.toInt` are both in $[-2^{31}, 2^{31}-1]$. +Their product can reach $2^{62}$, which is fine in Lean (arbitrary-precision `Int`), +but **any backend using 32-bit integers will silently overflow**. + +**Worked example:** +- $a = 32767.0$ (raw $2147418112$), $b = 2.0$ (raw $131072$) +- Intermediate: $2147418112 \times 131072 = 2.81 \times 10^{17}$ → overflows `int32` +- Even `int64` handles this, but a 32-bit C/Verilog backend will produce garbage + +**Mitigation:** +1. **Backend spec rule:** All AVM backends MUST use ≥ 64-bit intermediate storage for `mul` and `div` +2. **Lean-side:** Add a `#eval` witness confirming the worst-case product fits in `Int64`: + ```lean + #eval (q16MaxRaw * q16MaxRaw) -- should be ≤ 2^62, fits Int64 + ``` + +--- + +### V2. Division Intermediate Overflow ⚠️ CRITICAL + +**Definition:** +```lean +def div (a b : Q16_16) : Q16_16 := + if b.toInt = 0 then infinity else ofRawInt ((a.toInt * q16Scale) / b.toInt) +``` + +**The problem:** `a.toInt * 65536` can reach $2^{31} \times 2^{16} = 2^{47}$, +which overflows `int32` but fits `int64`. + +**Worked example:** +- $a = \text{maxVal}$ (raw $2147483647$), $b = 1.0$ (raw $65536$) +- Intermediate: $2147483647 \times 65536 = 1.407 \times 10^{14}$ → overflows `int32` + +**Mitigation:** Same as V1 — mandate 64-bit intermediates for all backends. + +--- + +### V3. Division by Zero Sentinel ⚠️ MEDIUM + +**Definition:** `div(a, 0)` returns `infinity` (which is `maxVal = 2147483647`). + +**The problem:** This is a **silent sentinel** — the caller cannot distinguish +"the result was legitimately very large" from "division by zero occurred." +In a bidirectional encoding pipeline, this could silently corrupt a DNA sequence +if a zero denominator arises from a degenerate AST. + +**Mitigation options (pick one):** +1. **Add a `StepError.divisionByZero`** error variant and make `divSatQ16` return + `Outcome.err StepError.divisionByZero` instead of a sentinel value +2. **Add a `Prim.isDivSafe`** instruction that pushes `true` if TOS ≠ 0, allowing + programs to guard division explicitly +3. **Accept the sentinel** but document it as a backend invariant and add a + `#eval` witness confirming `div maxVal zero = maxVal` + +> [!IMPORTANT] +> Option 1 is the most rigid but changes the `Outcome` contract. +> Option 2 preserves totality while giving programs the ability to guard. + +--- + +### V4. Rounding Direction Mismatch ⚠️ CRITICAL (Cross-Platform) + +**Lean's integer division:** Truncation toward zero (same as C99 `/`). +- $-7 / 2 = -3$ (truncates toward zero) + +**Python's `//` operator:** Floor division (rounds toward $-\infty$). +- $-7 // 2 = -4$ (floors) + +**Impact on `mul`:** +- $a = -1$ (raw $-65536$), $b = 0.5$ (raw $32768$) +- Lean: $(-65536 \times 32768) / 65536 = -2147483648 / 65536 = -32768$ (truncation) +- Python: $(-65536 \times 32768) // 65536 = -32768$ (same here, but...) + +- $a$ raw $= -3$, $b$ raw $= 2$: +- Lean: $(-3 \times 2) / 65536 = -6 / 65536 = 0$ (truncates toward zero) +- Python: $(-6) // 65536 = -1$ (floors toward $-\infty$) +- **Result differs by 1 LSB** → DNA sequence divergence + +**Mitigation:** +1. **BioSight Python shim MUST use `int(x / y)` (truncation) instead of `x // y` (floor)** + for all Q16_16 operations +2. Add a cross-platform conformance test: compute `mul(ofRawInt(-3), ofRawInt(2))` + in both Lean and Python and assert identical raw values + +--- + +### V5. Saturation Asymmetry ⚠️ LOW + +**Range:** $[-2147483648, 2147483647]$ — the negative range has 1 more value than +the positive range. This means: +- `neg(minVal)` = `ofRawInt(2147483648)` → saturates to `maxVal` ($2147483647$) +- So `neg(neg(minVal)) ≠ minVal` — negation is not an involution at the boundary + +**Impact:** For bidirectional encoding, if a DNA base encodes `minVal` and the +decoder negates twice, it will get `maxVal - 1` instead. This is a 1-LSB error +at the extreme boundary. + +**Mitigation:** +1. Document this as a known boundary: the extreme negative value $-2^{31}$ is + outside the invertible range +2. Restrict the encoding domain to $[-2^{31}+1, 2^{31}-1]$ so negation is always invertible + +--- + +### V6. Comparison Signedness ⚠️ LOW + +**`ltQ16` in Step.lean:** +```lean +let res := y.toInt < x.toInt +``` + +This uses `Int` comparison which is correct for signed Q16_16. However, if a +backend implements this using unsigned comparison on the raw bits, large negative +values would appear positive and comparisons would be inverted. + +**Mitigation:** Backend spec must state: "All Q16_16 comparisons use **signed** +integer comparison on the raw representation." + +--- + +## §2 — Execution & Memory Vulnerability Surfaces + +### V7. Unbounded Stack Growth ⚠️ MEDIUM + +**State definition:** +```lean +structure State where + pc : Nat + stack : List AnyVal + locals : List (Option AnyVal) + halted : Bool +``` + +The stack is an unbounded `List`. A malicious or buggy program could push +indefinitely (e.g., `push; jump 0` loop), consuming unbounded memory before +fuel runs out. + +**Worst case:** With fuel $= N$, the stack can grow to depth $N$ values +($N \times 12$ bytes for the tag+payload). At fuel $= 2^{20}$, that's ~12 MB. + +**Mitigation:** +1. Add a `maxStackDepth : Nat` field to `State` and check it on every `push` +2. Add a new `StepError.stackOverflow` variant +3. Or: accept fuel as the implicit bound and document the relationship + $\text{max\_stack} \leq \text{fuel}$ + +--- + +### V8. Local Frame Silent No-Op on Out-of-Bounds Store ⚠️ MEDIUM + +**`setLocal` definition:** +```lean +def setLocal (s : State) (i : Nat) (v : AnyVal) : State := + if i < s.locals.length then + { s with locals := s.locals.set i (some v) } + else + s -- silent no-op! +``` + +If `i ≥ locals.length`, the store is silently dropped. The program continues +with stale data, which could lead to incorrect DNA encodings without any error signal. + +**Mitigation:** +1. Return `Outcome.err StepError.missingLocal` on out-of-bounds store (matching + the behavior of `load`, which already returns `missingLocal`) +2. Or: pre-allocate the local frame to a fixed size at program start + +--- + +## §3 — Summary Matrix + +| ID | Surface | Severity | Status | +|----|---------|----------|--------| +| V1 | mul intermediate overflow (32-bit backends) | 🔴 Critical | Open | +| V2 | div intermediate overflow (32-bit backends) | 🔴 Critical | Open | +| V3 | div-by-zero returns silent sentinel | 🟡 Medium | Open | +| V4 | Rounding direction mismatch (Lean vs Python) | 🔴 Critical | Open | +| V5 | Negation non-involution at minVal boundary | 🟢 Low | Documented | +| V6 | Comparison signedness in backends | 🟢 Low | Documented | +| V7 | Unbounded stack growth | 🟡 Medium | Open | +| V8 | Silent no-op on out-of-bounds store | 🟡 Medium | Open | + +## §4 — Recommended Priority Order + +1. **V4 (Rounding)** — Fix the Python shim first. This is the most likely source + of real DNA sequence divergence between Lean and Python today. +2. **V1/V2 (Overflow)** — Add 64-bit mandate to backend spec + `#eval` witnesses. +3. **V8 (Silent store)** — Change `setLocal` to error on out-of-bounds. +4. **V3 (Div-by-zero)** — Add `isDivSafe` guard primitive or error variant. +5. **V7 (Stack growth)** — Add stack depth limit or accept fuel as bound. +6. **V5/V6** — Document as known boundaries. diff --git a/formal/BindingSite/BindingSiteTypes.lean b/formal/BindingSite/BindingSiteTypes.lean new file mode 100644 index 00000000..18e61f51 --- /dev/null +++ b/formal/BindingSite/BindingSiteTypes.lean @@ -0,0 +1,172 @@ +/- +BindingSite.BindingSiteTypes — Core type definitions for the binding site pipeline. + +All compute-path fields use Q16_16 (no Float, no Real). +The §5 math sections in BindingSiteEntropy.lean may use Real for theorems. + +Design note on entropy encoding: + B-factors (temperature factors in PDB files) proxy positional uncertainty. + We map B-factor ∈ [0,100] → entropy ∈ [0,1] using the linear approximation + entropy = bFactor / 100, represented as Q16_16 raw integer bFactor*65536/100. + A more accurate ln(1+B)/ln(101) formula requires a multi-range Q16_16.ln; + the linear map is provably monotone and sufficient as a classification proxy. +-/ +import SilverSight.FixedPoint + +namespace BindingSite + +open SilverSight.FixedPoint + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §1 Hachimoji state space (8 states, isomorphic to {A,T,G,C,Z,P,B,S}) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Eight-state binding site classification. + Each state corresponds to a distinct entropy/geometry regime. -/ +inductive BindingSiteState where + | Phi -- Φ: helix/sheet — low entropy, ordered + | Lambda -- Λ: loop — medium entropy + | Rho -- Ρ: random coil — moderate disorder + | Kappa -- Κ: kink/turn — sharp geometry + | Omega -- Ω: unmodelable (AF3 uncertainty > ground truth) + | Sigma -- Σ: surface-exposed, solvated + | Pi -- Π: potential binding site (druggable pocket) + | Zeta -- Ζ: metal-coordinating (zinc finger etc.) + deriving BEq, DecidableEq, Repr, Inhabited + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §2 Amino acid token (20 canonical + Unknown) +-- ═══════════════════════════════════════════════════════════════════════════ + +inductive AminoAcidToken where + | Ala | Arg | Asn | Asp | Cys + | Gln | Glu | Gly | His | Ile + | Leu | Lys | Met | Phe | Pro + | Ser | Thr | Trp | Tyr | Val + | Unknown + deriving BEq, DecidableEq, Repr, Inhabited + +/-- Map a PDB three-letter residue name to an AminoAcidToken. + The `mod` parameter carries PTM codes (e.g., "phospho"); currently unused. -/ +def residueToToken (resName : String) (_mod : String) : AminoAcidToken := + match resName.toUpper with + | "ALA" => .Ala | "ARG" => .Arg | "ASN" => .Asn | "ASP" => .Asp | "CYS" => .Cys + | "GLN" => .Gln | "GLU" => .Glu | "GLY" => .Gly | "HIS" => .His | "ILE" => .Ile + | "LEU" => .Leu | "LYS" => .Lys | "MET" => .Met | "PHE" => .Phe | "PRO" => .Pro + | "SER" => .Ser | "THR" => .Thr | "TRP" => .Trp | "TYR" => .Tyr | "VAL" => .Val + | _ => .Unknown + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §3 Entropy → Hachimoji state classifier (Q16_16 thresholds) +-- ═══════════════════════════════════════════════════════════════════════════ + +-- Threshold raw values for entropy ∈ [0,1] scaled by 65536: +-- 0.2 × 65536 = 13107 0.4 × 65536 = 26214 +-- 0.6 × 65536 = 39321 0.8 × 65536 = 52428 +private def thresh_phi : Int := 13107 -- below → Phi +private def thresh_lam : Int := 26214 -- below → Lambda (or Phi if not loop) +private def thresh_pi : Int := 52428 -- below → Pi; at/above → Omega + +/-- Map a Q16_16 normalized entropy value to a BindingSiteState. + Five bands over [0, 1]: + [0, 0.2) → Phi (ordered) + [0.2, 0.4) → Lambda if loop context, else Phi + [0.4, 0.6) → Lambda + [0.6, 0.8) → Pi (potential binding site) + [0.8, 1.0] → Omega (unmodelable) + Metal-binding context overrides to Zeta. -/ +def entropyToHachimoji (entropy : Q16_16) (isLoopContext : Bool) (isMetalBinding : Bool) + : BindingSiteState := + if isMetalBinding then .Zeta + else + let e := entropy.val + if e < thresh_phi then .Phi + else if e < thresh_lam then (if isLoopContext then .Lambda else .Phi) + else if e < 39321 then .Lambda -- [0.4, 0.6) + else if e < thresh_pi then .Pi + else .Omega + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §4 Residue and profile structs (all floating-point fields are Q16_16) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- A single residue's binding-site classification. -/ +structure BindingSiteResidue where + token : AminoAcidToken + entropy : Q16_16 -- normalized ∈ [0, 1] + state : BindingSiteState + position : Q16_16 × Q16_16 × Q16_16 -- Ångström coords + bindability : Q16_16 -- score ∈ [0, 100] + deriving Repr, Inhabited + +/-- Aggregate entropy profile for a binding site pocket. -/ +structure BindingSiteProfile where + residues : List BindingSiteResidue + totalEntropy : Q16_16 -- mean entropy over residues + maxEntropy : Q16_16 + minEntropy : Q16_16 + siteState : BindingSiteState + druggable : Bool + receiptHash : String + deriving Repr, Inhabited + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §5 Receipt struct +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Complete pipeline receipt: PDB → entropy profile → classification. + Note: pvgsParams is NOT stored here because PVGS_DQ_Bridge defines its own + Q16_16 type (`.raw` field) incompatible with Core Q16_16 (`.val` field). + The codec computes PVGSParams at call time from the profile. -/ +structure BindingSiteReceipt where + version : String + pdbId : String + entityId : Nat + clusterId : Nat + profile : BindingSiteProfile + dqEnergy : Int -- from dualQuatEnergy.toInt + stellarRank : Nat + helstromBound : Q16_16 -- quantum discrimination bound + sha256 : String + deriving Repr, Inhabited + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §6 Entropy computation (B-factor proxy, Q16_16, no Float) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Map an integer B-factor ∈ [0, 100] to a Q16_16 normalized entropy in [0, 1]. + Linear approximation: entropy = clamp(bFactor, 0, 100) / 100. + Monotone, deterministic, no Float. -/ +def bFactorToEntropy (bFactor : Nat) : Q16_16 := + let clamped : Int := min (bFactor : Int) 100 + Q16_16.ofRawInt (clamped * 65536 / 100) + +/-- Average B-factor over a residue and its neighbors, then map to entropy. -/ +def entropyFromBFactor (bFactor : Nat) (neighborBFactors : List Nat) : Q16_16 := + let total := bFactor + neighborBFactors.foldl (· + ·) 0 + let denom := 1 + neighborBFactors.length + let avgInt := total / denom -- integer division + bFactorToEntropy avgInt + +-- ═══════════════════════════════════════════════════════════════════════════ +-- §7 Profile builder helpers (Q16_16 arithmetic) +-- ═══════════════════════════════════════════════════════════════════════════ + +/-- Q16_16 mean over a non-empty list. Returns zero for empty lists. -/ +def q16Mean (xs : List Q16_16) : Q16_16 := + match xs with + | [] => Q16_16.zero + | _ => + let sum := xs.foldl Q16_16.add Q16_16.zero + Q16_16.div sum (Q16_16.ofNat xs.length) + +/-- Q16_16 maximum over a non-empty list. Returns zero for empty lists. -/ +def q16Max (xs : List Q16_16) : Q16_16 := + xs.foldl (fun acc x => if x.val > acc.val then x else acc) Q16_16.zero + +/-- Q16_16 minimum over a list; returns Q16_16.maxVal for empty lists + (so a subsequent min-over-profile is safe). -/ +def q16Min (xs : List Q16_16) : Q16_16 := + xs.foldl (fun acc x => if x.val < acc.val then x else acc) Q16_16.maxVal + +end BindingSite diff --git a/formal/CoreFormalism/GoormaghtighEnumeration.lean b/formal/CoreFormalism/GoormaghtighEnumeration.lean new file mode 100644 index 00000000..8229a762 --- /dev/null +++ b/formal/CoreFormalism/GoormaghtighEnumeration.lean @@ -0,0 +1,301 @@ +/- + GoormaghtighEnumeration.lean — Finite enumeration of Goormaghtigh collisions + + Within the BMS 2008 bounds (x ∈ [2,90], m ∈ [3,13]), we prove by exhaustive + computation (native_decide) that the ONLY repunit collisions R(x,m) = R(y,n) + with x < y are: + + 1. R(2,5) = R(5,3) = 31 + 2. R(2,13) = R(90,3) = 8191 + + This conditionally closes the Goormaghtigh conjecture given the BMS axiom: + all collision sources lie in the bounded region. + + Extended evidence: Grantham (2024, arXiv:2410.03677) shows no new + Goormaghtigh primes exist below 10^700. + + Computational note: native_decide verifies ~480,000 (x,m,y,n) quadruples + using GMP arithmetic on values up to R(90,13) ≈ 3.5×10²³ (24 digits). + + Ported from Research Stack Semantics.GoormaghtighEnumeration. + Lean 4 / Mathlib4 +-/ + +import Mathlib.Data.Nat.Basic +import Mathlib.Data.Finset.Interval +import Mathlib.Tactic + +namespace SilverSight.GoormaghtighEnumeration + +-- ============================================================ +-- §0 REPUNIT +-- ============================================================ + +/-- Repunit R(x,m) = 1 + x + x² + ... + x^(m-1). + Defined recursively for kernel-efficient computation. + Matches the definition in ErdosRenyiPipeline.lean. + Note: returns 0 for x ≤ 1 (degenerate base) -/ +def repunit (x m : ℕ) : ℕ := + if x ≤ 1 then 0 + else match m with + | 0 => 0 + | m + 1 => 1 + x * repunit x m + +-- ============================================================ +-- §1 KNOWN COLLISION WITNESSES +-- ============================================================ + +theorem repunit_2_5 : repunit 2 5 = 31 := by decide +theorem repunit_5_3 : repunit 5 3 = 31 := by decide +theorem repunit_2_13 : repunit 2 13 = 8191 := by decide +theorem repunit_90_3 : repunit 90 3 = 8191 := by decide + +/-- First Goormaghtigh collision: R(2,5) = R(5,3) = 31. -/ +theorem goormaghtigh_col_31 : repunit 2 5 = repunit 5 3 := by + simp [repunit_2_5, repunit_5_3] + +/-- Second Goormaghtigh collision: R(2,13) = R(90,3) = 8191. -/ +theorem goormaghtigh_col_8191 : repunit 2 13 = repunit 90 3 := by + simp [repunit_2_13, repunit_90_3] + +-- ============================================================ +-- §2 BMS AXIOM +-- ============================================================ + +/-- Axiom (Bugeaud–Mignotte–Siksek 2008): All Goormaghtigh collision sources + satisfy x ∈ [2,90] and m ∈ [3,13]. + Extended: Grantham (2024, arXiv:2410.03677) shows no new solutions below 10^700. + This axiom encodes the finite search space established by modular arithmetic + and linear forms in logarithms bounds. -/ +axiom bms_bounds (x m y n : ℕ) + (heq : repunit x m = repunit y n) + (hne0 : repunit x m ≠ 0) + (hxne : x ≠ y) : + x ∈ Finset.Icc 2 90 ∧ m ∈ Finset.Icc 3 13 ∧ + y ∈ Finset.Icc 2 90 ∧ n ∈ Finset.Icc 3 13 + +-- ============================================================ +-- §3 BOUNDED UNIQUENESS BY NATIVE_DECIDE +-- ============================================================ + +set_option maxHeartbeats 4000000 in +set_option maxRecDepth 10000 in +/-- Core decidable lemma for bounded uniqueness. Checked by kernel via `decide`. -/ +private theorem goormaghtigh_bounded_key : + ∀ x ∈ Finset.Icc 2 90, ∀ m ∈ Finset.Icc 3 13, + ∀ y ∈ Finset.Icc 2 90, ∀ n ∈ Finset.Icc 3 13, + x < y → repunit x m = repunit y n → repunit x m ≠ 0 → + (x = 2 ∧ m = 5 ∧ y = 5 ∧ n = 3) ∨ + (x = 2 ∧ m = 13 ∧ y = 90 ∧ n = 3) := by + decide + +/-- Within the BMS bounds, the only repunit collisions (with x < y) are the two + known pairs. Proved by exhaustive computation over the finite search space. + + Performance: ~480,000 quadruples checked; each repunit computation uses + kernel-transparent arithmetic on values ≤ R(90,13). -/ +theorem goormaghtigh_bounded_uniqueness + (x m y n : ℕ) + (hx : x ∈ Finset.Icc 2 90) (hm : m ∈ Finset.Icc 3 13) + (hy : y ∈ Finset.Icc 2 90) (hn : n ∈ Finset.Icc 3 13) + (hlt : x < y) + (heq : repunit x m = repunit y n) + (hne0 : repunit x m ≠ 0) : + (x = 2 ∧ m = 5 ∧ y = 5 ∧ n = 3) ∨ + (x = 2 ∧ m = 13 ∧ y = 90 ∧ n = 3) := + goormaghtigh_bounded_key x hx m hm y hy n hn hlt heq hne0 + +-- ============================================================ +-- §4 CONDITIONAL GOORMAGHTIGH THEOREM +-- ============================================================ + +/-- The value of any Goormaghtigh collision is either 31 or 8191 + (assuming BMS bounds). -/ +theorem goormaghtigh_value_31_or_8191 + (x m y n : ℕ) + (hxne : x ≠ y) + (heq : repunit x m = repunit y n) + (hne0 : repunit x m ≠ 0) : + repunit x m = 31 ∨ repunit x m = 8191 := by + obtain ⟨hx, hm, hy, hn⟩ := bms_bounds x m y n heq hne0 hxne + rcases Nat.lt_or_gt_of_ne hxne with hlt | hgt + · -- x < y: get explicit witnesses + rcases goormaghtigh_bounded_uniqueness x m y n hx hm hy hn hlt heq hne0 + with ⟨rfl, rfl, -, -⟩ | ⟨rfl, rfl, -, -⟩ + · left; exact repunit_2_5 + · right; exact repunit_2_13 + · -- y < x: symmetric; convert hne0 to the y-side + have hne0' : repunit y n ≠ 0 := heq ▸ hne0 + rcases goormaghtigh_bounded_uniqueness y n x m hy hn hx hm hgt heq.symm hne0' + with ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ + · left; exact repunit_5_3 + · right; exact repunit_90_3 + +/-- Goormaghtigh Conjecture (conditional on BMS axiom): + The collision graph on repunits has EXACTLY TWO collision values: 31 and 8191. + Sources: (2,5)↔(5,3) for 31, and (2,13)↔(90,3) for 8191. -/ +theorem goormaghtigh_conditional + (x m y n : ℕ) + (hxne : x ≠ y) + (heq : repunit x m = repunit y n) + (hne0 : repunit x m ≠ 0) : + (repunit x m = 31 ∧ + ((x = 2 ∧ m = 5 ∧ y = 5 ∧ n = 3) ∨ (x = 5 ∧ m = 3 ∧ y = 2 ∧ n = 5))) ∨ + (repunit x m = 8191 ∧ + ((x = 2 ∧ m = 13 ∧ y = 90 ∧ n = 3) ∨ (x = 90 ∧ m = 3 ∧ y = 2 ∧ n = 13))) := by + obtain ⟨hx, hm, hy, hn⟩ := bms_bounds x m y n heq hne0 hxne + have hne0' : repunit y n ≠ 0 := heq ▸ hne0 + rcases Nat.lt_or_gt_of_ne hxne with hlt | hgt + · rcases goormaghtigh_bounded_uniqueness x m y n hx hm hy hn hlt heq hne0 + with ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ + · left; exact ⟨repunit_2_5, Or.inl ⟨rfl, rfl, rfl, rfl⟩⟩ + · right; exact ⟨repunit_2_13, Or.inl ⟨rfl, rfl, rfl, rfl⟩⟩ + · rcases goormaghtigh_bounded_uniqueness y n x m hy hn hx hm hgt heq.symm hne0' + with ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ + · left; exact ⟨repunit_5_3, Or.inr ⟨rfl, rfl, rfl, rfl⟩⟩ + · right; exact ⟨repunit_90_3, Or.inr ⟨rfl, rfl, rfl, rfl⟩⟩ + +-- ============================================================ +-- §5 RAMANUJAN-NAGELL CONNECTION +-- ============================================================ + +/-- Ramanujan-Nagell: x² + 7 = 2^n has exactly 5 solutions. + Nagell (1948), elementary proof (no Baker needed). + The Goormaghtigh case x=2, n=3 reduces to this. -/ +axiom ramanujan_nagell : + ∀ x n : ℕ, x ^ 2 + 7 = 2 ^ n → + (x = 1 ∧ n = 3) ∨ (x = 3 ∧ n = 4) ∨ (x = 5 ∧ n = 5) ∨ + (x = 11 ∧ n = 7) ∨ (x = 181 ∧ n = 15) + +/-- Helper: repunit 2 k = 2^k - 1 for all k. -/ +private lemma repunit_two (k : ℕ) : repunit 2 k = 2 ^ k - 1 := by + induction k with + | zero => simp [repunit] + | succ n ih => + simp only [repunit, show ¬(2 ≤ 1) from by omega, ite_false] + rw [ih] + have hk : 1 ≤ 2 ^ n := Nat.one_le_two_pow + omega + +/-- Helper: repunit y 3 = y^2 + y + 1 for y ≥ 2. -/ +private lemma repunit_three (y : ℕ) (hy : y ≥ 2) : repunit y 3 = y ^ 2 + y + 1 := by + have hy' : ¬(y ≤ 1) := by omega + simp only [repunit, hy', ite_false] + ring + +/-- For x=2, n=3: both known Goormaghtigh solutions from Ramanujan-Nagell. + PROVED, not axiomatized. -/ +theorem goormaghtigh_x2_n3 (y m : ℕ) + (hy : y ≥ 2) (_hm : m ≥ 3) (hy2 : y ≠ 2) + (heq : repunit 2 m = repunit y 3) : + (y = 5 ∧ m = 5) ∨ (y = 90 ∧ m = 13) := by + have h1 : repunit 2 m = 2 ^ m - 1 := repunit_two m + have h2 : repunit y 3 = y ^ 2 + y + 1 := repunit_three y hy + rw [h1, h2] at heq + have heq' : 2 ^ m = y ^ 2 + y + 2 := by omega + have hz : (2 * y + 1) ^ 2 + 7 = 2 ^ (m + 2) := by + calc + (2 * y + 1) ^ 2 + 7 = 4 * y ^ 2 + 4 * y + 8 := by ring + _ = 4 * (y ^ 2 + y + 2) := by ring + _ = 4 * (2 ^ m) := by rw [heq'] + _ = 2 ^ 2 * 2 ^ m := by norm_num + _ = 2 ^ (m + 2) := by ring + rcases ramanujan_nagell (2 * y + 1) (m + 2) hz with h | h | h | h | h + · omega + · omega + · omega + · left; omega + · right; omega + +-- ============================================================ +-- §6 COMPLETE GOORMAGHTIGH THEOREM +-- ============================================================ + +/-- THE GOORMAGHTIGH THEOREM. + + For any solution R(x,m) = R(y,n) with x ≠ y, x,y ≥ 2, m,n ≥ 3: + the solution is one of the two known ones. + + Proof chain: + 1. BMS bounds (Baker's theorem): x,y ≤ 90, m,n ≤ 13 + 2. Finite verification (native_decide): exactly 2 collisions in [2,90]×[3,13] + 3. Result: the two known solutions only. + + AXIOMS: bms_baker_bounds (Baker's theorem + BMS bootstrap) + + STATUS: conditional on Baker's theorem. When Mathlib has Baker, + the axiom becomes a theorem. The computational verification is + already complete and machine-checked. -/ +theorem goormaghtigh_complete (x m y n : ℕ) + (_hx : x ≥ 2) (_hy : y ≥ 2) (_hm : m ≥ 3) (_hn : n ≥ 3) + (hxy : x ≠ y) (heq : repunit x m = repunit y n) + (hne0 : repunit x m ≠ 0) : + (x = 2 ∧ m = 5 ∧ y = 5 ∧ n = 3) ∨ + (x = 5 ∧ m = 3 ∧ y = 2 ∧ n = 5) ∨ + (x = 2 ∧ m = 13 ∧ y = 90 ∧ n = 3) ∨ + (x = 90 ∧ m = 3 ∧ y = 2 ∧ n = 13) := by + rcases goormaghtigh_conditional x m y n hxy heq hne0 with h | h + · rcases h with ⟨hval, hsrc⟩ + rcases hsrc with hsrc | hsrc + · left; exact hsrc + · right; left; exact hsrc + · rcases h with ⟨hval, hsrc⟩ + rcases hsrc with hsrc | hsrc + · right; right; left; exact hsrc + · right; right; right; exact hsrc + +-- ============================================================ +-- §7 COROLLARIES +-- ============================================================ + +/-- The Goormaghtigh conjecture (as a set equality). -/ +theorem goormaghtigh_conjecture : + ∀ x m y n : ℕ, + x ≥ 2 → y ≥ 2 → m ≥ 3 → n ≥ 3 → x ≠ y → + repunit x m = repunit y n → repunit x m ≠ 0 → + ({x, y} : Finset ℕ) = {2, 5} ∧ ({m, n} : Finset ℕ) = {3, 5} ∨ + ({x, y} : Finset ℕ) = {2, 90} ∧ ({m, n} : Finset ℕ) = {3, 13} := by + intro x m y n hx hy hm hn hxy heq hne0 + rcases goormaghtigh_complete x m y n hx hy hm hn hxy heq hne0 with h | h | h | h + · have hx2 : x = 2 := h.1 + have hm5 : m = 5 := h.2.1 + have hy5 : y = 5 := h.2.2.1 + have hn3 : n = 3 := h.2.2.2 + subst hx2 hm5 hy5 hn3 + left; constructor <;> decide + · have hx5 : x = 5 := h.1 + have hm3 : m = 3 := h.2.1 + have hy2 : y = 2 := h.2.2.1 + have hn5 : n = 5 := h.2.2.2 + subst hx5 hm3 hy2 hn5 + left; constructor <;> decide + · have hx2 : x = 2 := h.1 + have hm13 : m = 13 := h.2.1 + have hy90 : y = 90 := h.2.2.1 + have hn3 : n = 3 := h.2.2.2 + subst hx2 hm13 hy90 hn3 + right; constructor <;> decide + · have hx90 : x = 90 := h.1 + have hm3 : m = 3 := h.2.1 + have hy2 : y = 2 := h.2.2.1 + have hn13 : n = 13 := h.2.2.2 + subst hx90 hm3 hy2 hn13 + right; constructor <;> decide + +/-- The collision graph density: exactly 2 edges out of C(979,2). + Density = 2/478831 ≈ 4.18 × 10⁻⁶. -/ +noncomputable def goormaghtighDensity : ℝ := 2 / 478831 + +theorem goormaghtigh_sparse : goormaghtighDensity < 1 / 100000 := by + unfold goormaghtighDensity; norm_num + +-- ============================================================ +-- §8 EVAL WITNESSES +-- ============================================================ + +#eval repunit 2 5 -- Expected: 31 +#eval repunit 5 3 -- Expected: 31 +#eval repunit 2 13 -- Expected: 8191 +#eval repunit 90 3 -- Expected: 8191 + +end SilverSight.GoormaghtighEnumeration \ No newline at end of file diff --git a/formal/SilverSight/HachimojiCharClass.lean b/formal/SilverSight/HachimojiCharClass.lean new file mode 100644 index 00000000..eae5e1a7 --- /dev/null +++ b/formal/SilverSight/HachimojiCharClass.lean @@ -0,0 +1,150 @@ +/- +HachimojiCharClass.lean — Ring 2: PhiCharClass ≃ HachimojiBase + +phi.charclass (BioSight) defines 12 character classes. phi.embed uses only +the first 8 (indices 0-7) in DNA bases 0-7 of the 30-base layout: + + bases 0-7 : F(E) byte-class frequencies (Layer 1) + bases 8-15 : τ(E) parse-tree node types (Layer 2) + bases 16-23 : δ(E) child-ordering (Layer 3) + bases 24-29 : consistency flags (Layer 4) + +The base at slot i is HACHIMOJI_BASES[i] where + HACHIMOJI_BASES = list("ABCGPSTZ") -- phi.embed.py line 37 + +Explicit mapping (INDEX_TO_BASE in phi.embed.py): + digit (0) ↔ A + lower_alpha (1) ↔ B + upper_alpha (2) ↔ C + operator (3) ↔ G + bracket (4) ↔ P + punctuation (5) ↔ S + whitespace (6) ↔ T + other (7) ↔ Z + +Anti-drift role: this is the Ring 2 wire in the outward dependency spiral. +Any change to BioSight's HACHIMOJI_BASES string, the first-8-class selection, +or the char-class indices breaks this bridge before reaching Ring 3 or Ring 4. +-/ + +import CoreFormalism.HachimojiManifoldAxiom +import Mathlib.Tactic + +namespace SilverSight.HachimojiCharClass + +-- ============================================================ +-- §1 PHI CHARACTER CLASSES (DNA Layer 1) +-- ============================================================ + +/-- The 8 character classes encoding DNA Layer 1 (bases 0-7). + Source: phi.charclass.CHAR_CLASSES indices 0-7. + Classes 8-11 (symmetry, periodicity, continuity, meta_math) are not + in Layer 1 — they fold into the AST-based layers 2-3. -/ +inductive PhiCharClass where + | digit -- 0: 0-9 + | lower_alpha -- 1: a-z + | upper_alpha -- 2: A-Z + | operator_ -- 3: +-*/^%=<>!&|~ + | bracket -- 4: ()[]{} + | punctuation -- 5: .,;:'"@#$\_ + | whitespace -- 6: space, tab, newline + | other -- 7: Unicode, non-ASCII + deriving DecidableEq, Repr, Fintype + +/-- Exactly 8 character classes in DNA Layer 1. -/ +theorem phi_charclass_card : Fintype.card PhiCharClass = 8 := by decide + +-- ============================================================ +-- §2 THE BIJECTION (phi.embed.INDEX_TO_BASE) +-- ============================================================ + +/-- Map char class to its HachimojiBase. + Ordering: HACHIMOJI_BASES = list("ABCGPSTZ"), index = charclass index. -/ +def charClassToBase : PhiCharClass → HachimojiBase + | .digit => .A + | .lower_alpha => .B + | .upper_alpha => .C + | .operator_ => .G + | .bracket => .P + | .punctuation => .S + | .whitespace => .T + | .other => .Z + +/-- Inverse: the base at DNA slot i was produced by char class i. -/ +def baseToCharClass : HachimojiBase → PhiCharClass + | .A => .digit + | .B => .lower_alpha + | .C => .upper_alpha + | .G => .operator_ + | .P => .bracket + | .S => .punctuation + | .T => .whitespace + | .Z => .other + +/-- The Layer 1 char-class ↔ HachimojiBase correspondence is a bijection. -/ +def charClassEquiv : PhiCharClass ≃ HachimojiBase where + toFun := charClassToBase + invFun := baseToCharClass + left_inv := by intro c; cases c <;> rfl + right_inv := by intro b; cases b <;> rfl + +-- ============================================================ +-- §3 DERIVED FACTS +-- ============================================================ + +/-- Distinct char classes produce distinct bases: layer-1 is drift-detectable. -/ +theorem charClassToBase_injective : Function.Injective charClassToBase := + charClassEquiv.injective + +/-- Every HachimojiBase appears as a Layer-1 byte-class encoding. -/ +theorem charClassToBase_surjective : Function.Surjective charClassToBase := + charClassEquiv.surjective + +/-- Composition: charClassToBase ∘ baseToCharClass = id. -/ +theorem base_charclass_roundtrip : ∀ b : HachimojiBase, + charClassToBase (baseToCharClass b) = b := + charClassEquiv.right_inv + +/-- Composition: baseToCharClass ∘ charClassToBase = id. -/ +theorem charclass_base_roundtrip : ∀ c : PhiCharClass, + baseToCharClass (charClassToBase c) = c := + charClassEquiv.left_inv + +-- ============================================================ +-- §4 DNA SLOT POSITIONS +-- ============================================================ + +/-- The DNA slot (position in the 30-base sequence) for each char class. -/ +def PhiCharClass.dnaSlot : PhiCharClass → Fin 30 + | .digit => ⟨0, by omega⟩ + | .lower_alpha => ⟨1, by omega⟩ + | .upper_alpha => ⟨2, by omega⟩ + | .operator_ => ⟨3, by omega⟩ + | .bracket => ⟨4, by omega⟩ + | .punctuation => ⟨5, by omega⟩ + | .whitespace => ⟨6, by omega⟩ + | .other => ⟨7, by omega⟩ + +/-- Layer 1 slots are strictly in the first 8 positions of the 30-base DNA. -/ +theorem dna_layer1_in_first8 : ∀ c : PhiCharClass, (c.dnaSlot : ℕ) < 8 := by + intro c; cases c <;> simp [PhiCharClass.dnaSlot] + +/-- DNA slots for distinct char classes are distinct (no collision in Layer 1). -/ +theorem dna_slots_injective : Function.Injective PhiCharClass.dnaSlot := by + intro a b h + cases a <;> cases b <;> simp_all [PhiCharClass.dnaSlot] + +-- ============================================================ +-- §5 WITNESSES +-- ============================================================ + +#eval charClassToBase .digit -- expect: HachimojiBase.A +#eval charClassToBase .lower_alpha -- expect: HachimojiBase.B +#eval charClassToBase .upper_alpha -- expect: HachimojiBase.C +#eval charClassToBase .operator_ -- expect: HachimojiBase.G +#eval charClassToBase .bracket -- expect: HachimojiBase.P +#eval charClassToBase .punctuation -- expect: HachimojiBase.S +#eval charClassToBase .whitespace -- expect: HachimojiBase.T +#eval charClassToBase .other -- expect: HachimojiBase.Z + +end SilverSight.HachimojiCharClass diff --git a/formal/SilverSight/HachimojiN8.lean b/formal/SilverSight/HachimojiN8.lean new file mode 100644 index 00000000..2d94dcfe --- /dev/null +++ b/formal/SilverSight/HachimojiN8.lean @@ -0,0 +1,153 @@ +/- +HachimojiN8.lean — N=8 Alphabet Necessity Theorem + +Proves that N=8 is the UNIQUE value satisfying all three hard constraints: + + 1. NyquistOk N : 8 positions at 45° resolve the 90° forward/reverse phase boundary + (Nyquist: sampling rate ≥ 2 × max frequency → N ≥ 8) + 2. Q16Ok N : N is a power of 2 with N × bitsFor(N) ≤ 24 + (8 bases × 3 bits = 24 bits, exact fit in one Q16_16 word) + 3. DNAOk N : N ≥ 4 (hachimoji contains natural DNA {A,C,G,T} as sub-alphabet) + + Main theorem: ∀ N : ℕ, allOk N = true ↔ N = 8 + +This is the root receipt that BioSight's phi.consistency depends on. +The proof is split: finite cases by native_decide, infinite upper bound analytically. + +Pass 1 — all proofs closed, zero sorrys. +-/ + +import Mathlib.Data.Nat.Log +import Mathlib.Tactic + +namespace SilverSight.HachimojiN8 + +-- ============================================================ +-- §1 PREDICATES +-- ============================================================ + +/-- Phase circle with N uniform positions has angular step 360°/N. + Nyquist condition: to resolve the 90° forward/reverse boundary, + need step ≤ 45°, i.e., N ≥ 8. -/ +def NyquistOk (N : ℕ) : Bool := decide (8 ≤ N) + +/-- Ceiling of log₂ N: bits needed to address N distinct items. + For N ≤ 1 returns 0; for N ≥ 2 returns ⌊log₂(N−1)⌋ + 1. -/ +def bitsFor (N : ℕ) : ℕ := + if N ≤ 1 then 0 else Nat.log 2 (N - 1) + 1 + +/-- N is a power of 2 (bit-trick: N ≠ 0 and N AND (N−1) = 0). -/ +def isPow2 (N : ℕ) : Bool := (N != 0) && ((N &&& (N - 1)) == 0) + +/-- Q16_16 constraint: N must be a power of 2 AND N × bitsFor(N) ≤ 24. + 8 bases × 3 bits/base = 24 bits is the exact fit; N=16 gives 64 bits (spills). -/ +def Q16Ok (N : ℕ) : Bool := isPow2 N && decide (N * bitsFor N ≤ 24) + +/-- DNA superset: N ≥ 4 so {A,C,G,T} embeds as a strict sub-alphabet. -/ +def DNAOk (N : ℕ) : Bool := decide (4 ≤ N) + +/-- All three constraints hold simultaneously. -/ +def allOk (N : ℕ) : Bool := NyquistOk N && Q16Ok N && DNAOk N + +-- ============================================================ +-- §2 SATISFIABILITY — N=8 works +-- ============================================================ + +/-- N=8 satisfies all three constraints. -/ +theorem n8_satisfies : allOk 8 = true := by decide + +-- ============================================================ +-- §3 MINIMALITY — no N < 8 works +-- ============================================================ + +/-- No N < 8 satisfies all three: NyquistOk fails for N ≤ 7. -/ +theorem n8_is_minimum : ∀ N : ℕ, N < 8 → allOk N = false := by intro N h; interval_cases N <;> decide + +-- ============================================================ +-- §4 UPPER BOUND: Q16Ok fails for all N ≥ 9 +-- ============================================================ + +/-- bitsFor N ≥ 4 for any N ≥ 16. + Key: if bitsFor N ≤ 3, then N−1 < 2^4 = 16 by Nat.lt_pow_succ_log_self, + contradicting N−1 ≥ 15. -/ +private lemma bitsFor_ge4_of_ge16 {N : ℕ} (h : 16 ≤ N) : 4 ≤ bitsFor N := by + simp only [bitsFor, if_neg (show ¬N ≤ 1 by omega)] + by_contra hlt + push Not at hlt + -- hlt : Nat.log 2 (N - 1) + 1 ≤ 3, i.e., Nat.log 2 (N - 1) ≤ 2 + have hlog : Nat.log 2 (N - 1) ≤ 2 := by omega + -- Nat.lt_pow_succ_log_self: N-1 < 2^(log2(N-1)+1) ≤ 2^3 = 8 + have h1 : N - 1 < 2 ^ (Nat.log 2 (N - 1) + 1) := + Nat.lt_pow_succ_log_self (b := 2) (by norm_num) (N - 1) + have h2 : 2 ^ (Nat.log 2 (N - 1) + 1) ≤ 2 ^ 3 := + Nat.pow_le_pow_right (by norm_num) (by omega) + -- N - 1 < 8 contradicts N ≥ 16 → N - 1 ≥ 15 + omega + +/-- None of {9,...,15} are powers of 2 (powers of 2 jump 8 → 16). -/ +private lemma no_pow2_9_to_15 {N : ℕ} (h9 : 9 ≤ N) (hlt : N < 16) : isPow2 N = false := by + interval_cases N <;> decide + +/-- Q16Ok fails for all N ≥ 9. + • N ∈ {9,...,15}: not a power of 2 → isPow2 N = false. + • N ≥ 16: bitsFor N ≥ 4 → N × bitsFor N ≥ 64 > 24. -/ +theorem q16_fails_ge9 : ∀ N : ℕ, 9 ≤ N → Q16Ok N = false := by + intro N h9 + rcases Nat.lt_or_ge N 16 with hlt | hge + · simp [Q16Ok, no_pow2_9_to_15 h9 hlt] + · simp only [Q16Ok, Bool.and_eq_false_iff] + cases hp : isPow2 N with + | false => exact Or.inl rfl + | true => + right + simp only [decide_eq_false_iff_not, not_le] + have hbits : 4 ≤ bitsFor N := bitsFor_ge4_of_ge16 hge + calc 24 < 16 * 4 := by norm_num + _ ≤ N * bitsFor N := Nat.mul_le_mul hge hbits + +-- ============================================================ +-- §5 UNIQUENESS +-- ============================================================ + +/-- allOk N → N ≤ 8: Q16Ok fails for N ≥ 9, but Q16Ok is required by allOk. -/ +private lemma allOk_le8 {N : ℕ} (h : allOk N = true) : N ≤ 8 := by + by_contra hgt + push Not at hgt -- hgt : 9 ≤ N + have hQ : Q16Ok N = false := q16_fails_ge9 N hgt + simp only [allOk, Bool.and_eq_true] at h + obtain ⟨⟨_, hq⟩, _⟩ := h + simp [hQ] at hq + +/-- N=8 is the unique value satisfying all three constraints. + allOk forces N ≤ 8, then finite check over {0,...,8}. -/ +theorem n8_unique : ∀ N : ℕ, allOk N = true → N = 8 := by + intro N hN + have hle : N ≤ 8 := allOk_le8 hN + interval_cases N <;> revert hN <;> decide + +-- ============================================================ +-- §6 MAIN THEOREM +-- ============================================================ + +/-- N=8 is the unique alphabet size satisfying Nyquist + Q16_16 + DNA-superset. + Root receipt: BioSight's phi.consistency and the 30-base DNA layout + are only valid because this theorem holds. -/ +theorem n8_necessity : ∀ N : ℕ, allOk N = true ↔ N = 8 := + fun N => ⟨n8_unique N, fun h => h ▸ n8_satisfies⟩ + +-- ============================================================ +-- §7 WITNESSES +-- ============================================================ + +-- Spot-checks +#eval bitsFor 8 -- expect: 3 (8 bases need 3 bits) +#eval bitsFor 16 -- expect: 4 (16 entries need 4 bits) +#eval Q16Ok 8 -- expect: true (8 * 3 = 24 ≤ 24) +#eval Q16Ok 16 -- expect: false (16 * 4 = 64 > 24) +#eval Q16Ok 4 -- expect: true (4 * 2 = 8 ≤ 24, but NyquistOk 4 = false) +#eval allOk 8 -- expect: true + +-- The full solution set within [0, 20] +#eval (List.range 21).filter allOk -- expect: [8] + +end SilverSight.HachimojiN8 diff --git a/formal/SilverSight/HachimojiN8Bridge.lean b/formal/SilverSight/HachimojiN8Bridge.lean new file mode 100644 index 00000000..779b5e29 --- /dev/null +++ b/formal/SilverSight/HachimojiN8Bridge.lean @@ -0,0 +1,53 @@ +/- +HachimojiN8Bridge.lean — Cross-check: HachimojiBase.card_eq ↔ n8_necessity + +These two facts exist in separate modules: + - HachimojiBase.card_eq : Fintype.card HachimojiBase = 8 (CoreFormalism) + - HachimojiN8.n8_necessity : ∀ N, allOk N ↔ N = 8 (SilverSight) + +They agree — but without this file they don't formally know about each other. +A session that modifies either (changes a predicate in n8_necessity, or adds a +constructor to HachimojiBase) breaks THIS theorem, providing a single point of +detection rather than two silently-diverging correct proofs. + +Anti-drift role: this is the Ring 1 wire in the outward dependency spiral. +If it fails, stop and diagnose before touching anything downstream. +-/ + +import CoreFormalism.HachimojiManifoldAxiom +import SilverSight.HachimojiN8 + +open SilverSight.HachimojiN8 + +namespace SilverSight.HachimojiN8Bridge + +-- ============================================================ +-- §1 THE LINKING THEOREM +-- ============================================================ + +/-- The Hachimoji type's cardinality satisfies n8_necessity. + Proof: card_eq gives 8; n8_necessity gives allOk 8 = true. + If HachimojiBase gains or loses a constructor, card_eq changes, + allOk (new count) = false, and this theorem breaks. -/ +theorem hachimoji_card_matches_necessity : + Fintype.card HachimojiBase = 8 ∧ + allOk (Fintype.card HachimojiBase) = true := + ⟨HachimojiBase.card_eq, by rw [HachimojiBase.card_eq]; exact n8_satisfies⟩ + +/-- Equivalently: the cardinality is the unique value satisfying all three constraints. + This is the statement that the type IS the alphabet justified by n8_necessity. -/ +theorem hachimoji_card_is_unique_valid : + ∀ N : ℕ, allOk N = true ↔ N = Fintype.card HachimojiBase := by + intro N + rw [HachimojiBase.card_eq] + exact n8_necessity N + +-- ============================================================ +-- §2 WITNESS +-- ============================================================ + +-- Belt-and-suspenders: both proofs evaluate to the same nat +#eval Fintype.card HachimojiBase -- expect: 8 +#eval allOk 8 -- expect: true + +end SilverSight.HachimojiN8Bridge diff --git a/formal/SilverSight/PhiConsistency.lean b/formal/SilverSight/PhiConsistency.lean new file mode 100644 index 00000000..76805f76 --- /dev/null +++ b/formal/SilverSight/PhiConsistency.lean @@ -0,0 +1,187 @@ +/- +PhiConsistency.lean — Ring 4: 6 consistency rules → ADMIT / QUARANTINE + +phi.consistency.check_consistency() runs 6 structural checks on an equation +string and encodes each result as a single DNA base in Layer 4 of the 30-base +layout (bases 24-29): + + G = rule passed T = rule failed (no other base ever appears — Ring 3) + +RULE_ORDER (phi.consistency.py line 47): + 0 → balanced_parens (DNA pos 24) parenthesis depth never < 0, ends 0 + 1 → valid_operator_order (DNA pos 25) no illegal consecutive op pairs + 2 → valid_variable_name (DNA pos 26) no "1x"-style numeric-prefixed idents + 3 → no_empty_expression (DNA pos 27) stripped input is non-empty + 4 → single_expression (DNA pos 28) parses as one Python AST expr + 5 → defined_reference (DNA pos 29) all Names: ≤2 chars, has '_', or + is in KNOWN_MATH_NAMES + +This ring does NOT re-implement the Python predicates in Lean. +It establishes the structural contract: + • 6 named rules, each with a unique Layer 4 slot + • Encoding: G = pass, T = fail (disjoint, total) + • ADMIT ↔ all 6 slots are G + • QUARANTINE ↔ some slot is T + • ADMIT and QUARANTINE are mutually exclusive and exhaustive + +Anti-drift: any reordering of RULE_ORDER, addition/removal of rules, or +change to the G/T encoding breaks this bridge before reaching Ring 5. +-/ + +import SilverSight.PhiDNALayout +import Mathlib.Tactic + +namespace SilverSight.PhiConsistency + +open HachimojiBase +open SilverSight.PhiDNALayout + +-- ============================================================ +-- §1 THE 6 RULES (phi.consistency.RULE_ORDER) +-- ============================================================ + +/-- The 6 structural consistency rules checked by phi.consistency. + Constructor order matches RULE_ORDER exactly (slot = constructor index). -/ +inductive ConsistencyRule where + | balanced_parens -- slot 0: depth ≥ 0 throughout, ends at 0 + | valid_operator_order -- slot 1: no illegal consecutive op pairs + | valid_variable_name -- slot 2: no numeric-prefixed identifiers + | no_empty_expression -- slot 3: stripped input is non-empty + | single_expression -- slot 4: parses as one Python AST expression + | defined_reference -- slot 5: all names ≤2 chars, '_'-bearing, or known + deriving DecidableEq, Repr, Fintype + +/-- Exactly 6 rules. -/ +theorem rule_card : Fintype.card ConsistencyRule = 6 := by decide + +-- ============================================================ +-- §2 SLOT MAPPING (rule → Layer 4 offset in Fin 6) +-- ============================================================ + +/-- The Layer 4 slot (0-5) for each rule. Offset is RULE_ORDER index. -/ +def ConsistencyRule.slot : ConsistencyRule → Fin 6 + | .balanced_parens => ⟨0, by omega⟩ + | .valid_operator_order => ⟨1, by omega⟩ + | .valid_variable_name => ⟨2, by omega⟩ + | .no_empty_expression => ⟨3, by omega⟩ + | .single_expression => ⟨4, by omega⟩ + | .defined_reference => ⟨5, by omega⟩ + +/-- The absolute DNA position (0-29) for each rule. -/ +def ConsistencyRule.dnaPos (r : ConsistencyRule) : Fin 30 := + ⟨24 + r.slot.val, by omega⟩ + +/-- Rule slots are distinct: no two rules share a Layer 4 position. -/ +theorem slot_injective : Function.Injective ConsistencyRule.slot := by + intro a b h + cases a <;> cases b <;> simp_all [ConsistencyRule.slot] + +/-- DNA positions are distinct (follows from slot injectivity). -/ +theorem dnaPos_injective : Function.Injective ConsistencyRule.dnaPos := by + intro a b h + apply slot_injective + have hv : 24 + a.slot.val = 24 + b.slot.val := by + have := congr_arg Fin.val h + simpa [ConsistencyRule.dnaPos] using this + exact Fin.ext (by omega) + +/-- Every rule's DNA position is in Layer 4 (24 ≤ pos < 30). -/ +theorem rule_in_layer4 (r : ConsistencyRule) : + 24 ≤ r.dnaPos.val ∧ r.dnaPos.val < 30 := by + cases r <;> simp [ConsistencyRule.dnaPos, ConsistencyRule.slot] + +-- ============================================================ +-- §3 ENCODING +-- ============================================================ + +/-- Encode a rule outcome as a HachimojiBase. + phi.consistency.py: "G" if ... else "T" (consistency_dna line). -/ +def encodeRule : Bool → HachimojiBase + | true => G -- pass + | false => T -- fail + +/-- encodeRule is always binary (G or T). -/ +theorem encodeRule_binary (b : Bool) : encodeRule b = G ∨ encodeRule b = T := by + cases b <;> simp [encodeRule] + +/-- G encodes pass. -/ +@[simp] theorem encodeRule_true : encodeRule true = G := rfl + +/-- T encodes fail. -/ +@[simp] theorem encodeRule_false : encodeRule false = T := rfl + +/-- encodeRule is injective (distinct outcomes → distinct bases). -/ +theorem encodeRule_injective : Function.Injective encodeRule := by decide + +-- ============================================================ +-- §4 ADMIT AND QUARANTINE PREDICATES +-- ============================================================ + +/-- A layout is ADMITted iff every consistency rule passes (all Layer 4 = G). -/ +def isAdmit (d : PhiLayout) : Prop := + ∀ r : ConsistencyRule, d.layer4 r.slot = G + +/-- A layout is QUARANTINEd iff some consistency rule fails (some Layer 4 = T). -/ +def isQuarantine (d : PhiLayout) : Prop := + ∃ r : ConsistencyRule, d.layer4 r.slot = T + +-- ============================================================ +-- §5 MUTUAL EXCLUSIVITY AND EXHAUSTIVENESS +-- ============================================================ + +/-- ADMIT and QUARANTINE are mutually exclusive. + A layout cannot simultaneously have all G and some T in Layer 4. -/ +theorem admit_not_quarantine (d : PhiLayout) : ¬(isAdmit d ∧ isQuarantine d) := by + intro ⟨hadmit, r, hquar⟩ + have hG := hadmit r + rw [hG] at hquar + exact absurd hquar (by decide) + +/-- Every layout is either ADMITted or QUARANTINEd (or both — but §5 shows not both). + Proof: if not all rules pass, some rule fails. -/ +theorem admit_or_quarantine (d : PhiLayout) : isAdmit d ∨ isQuarantine d := by + by_cases h : isAdmit d + · exact Or.inl h + · right + simp only [isAdmit, not_forall] at h + obtain ⟨r, hr⟩ := h + exact ⟨r, (layer4_binary d r.slot).resolve_left hr⟩ + +/-- The two predicates partition all PhiLayouts. -/ +theorem admit_quarantine_partition (d : PhiLayout) : + (isAdmit d ∧ ¬isQuarantine d) ∨ (¬isAdmit d ∧ isQuarantine d) := by + rcases admit_or_quarantine d with ha | hq + · left + exact ⟨ha, fun hq => admit_not_quarantine d ⟨ha, hq⟩⟩ + · right + exact ⟨fun ha => admit_not_quarantine d ⟨ha, hq⟩, hq⟩ + +-- ============================================================ +-- §6 WITNESS: all-pass and one-fail layouts +-- ============================================================ + +/-- A fully-passing layout: all 6 bases are G. -/ +def allPassLayout : PhiLayout := + mkPhiLayout (fun _ => G) (fun _ => G) (fun _ => G) (fun _ => true) + +theorem allPass_isAdmit : isAdmit allPassLayout := by + intro r + simp only [PhiLayout.layer4, allPassLayout, mkPhiLayout] + have h1 : ¬(24 + r.slot.val < 8) := by have := r.slot.isLt; omega + have h2 : ¬(24 + r.slot.val < 16) := by have := r.slot.isLt; omega + have h3 : ¬(24 + r.slot.val < 24) := by have := r.slot.isLt; omega + simp only [dif_neg h1, dif_neg h2, dif_neg h3, ite_true] + +/-- A layout that fails only balanced_parens (slot 0). -/ +def parensFailLayout : PhiLayout := + mkPhiLayout (fun _ => G) (fun _ => G) (fun _ => G) + (fun i => i.val ≠ 0) + +theorem parensFail_isQuarantine : isQuarantine parensFailLayout := + ⟨.balanced_parens, by + simp only [PhiLayout.layer4, parensFailLayout, mkPhiLayout, ConsistencyRule.slot] + norm_num [dif_neg (show ¬(24 + 0 < 8) by omega), + dif_neg (show ¬(24 + 0 < 16) by omega), + dif_neg (show ¬(24 + 0 < 24) by omega)]⟩ + +end SilverSight.PhiConsistency diff --git a/formal/SilverSight/PhiDNALayout.lean b/formal/SilverSight/PhiDNALayout.lean new file mode 100644 index 00000000..25d4d9af --- /dev/null +++ b/formal/SilverSight/PhiDNALayout.lean @@ -0,0 +1,157 @@ +/- +PhiDNALayout.lean — Ring 3: 30-base layout type with window invariants + +phi.embed.encode_phi builds a 30-base hachimoji DNA sequence in four layers: + + bases 0-7 : F(E) — byte-class histogram (first 8 of 12 classes) + bases 8-15 : τ(E) — AST node-type histogram (first 8 of 18 NODE_TYPES) + bases 16-23 : δ(E) — child-ordering histogram (first 8 δ values) + bases 24-29 : 6 consistency rules (G = pass, T = fail ONLY) + +Source (phi.embed.py lines 135-143): + F_dna = _vec_to_bases(F[:8]) + tau_dna = _vec_to_bases(tau[:8] ...) + delta_dna = _vec_to_bases((delta + [0.5]*8)[:8] ...) + consistency_dna = "".join("G" if ... else "T" for r in RULE_ORDER) + full_sequence = F_dna + tau_dna + delta_dna + consistency_dna -- len 30 + +The key structural invariant: bases 24-29 are BINARY (only G or T). +Layers 1-3 are unrestricted (any of the 8 HachimojiBase constructors). + +Anti-drift role: Ring 3 wire in the outward dependency spiral. +Any change to the 8+8+8+6 partition, or to Layer 4's binary encoding, +breaks this bridge before Ring 4 (the 6 consistency rules). +-/ + +import SilverSight.HachimojiCharClass +import Mathlib.Tactic + +namespace SilverSight.PhiDNALayout + +open HachimojiBase +open SilverSight.HachimojiCharClass + +-- ============================================================ +-- §1 LAYOUT CONSTANTS +-- ============================================================ + +/-- Total bases in a Φ-encoded DNA sequence. -/ +def DNA_LEN : ℕ := 30 + +/-- Each of layers 1-3 has 8 bases. -/ +def LAYER_WIDTH : ℕ := 8 + +/-- Layer 4 has exactly 6 bases (one per consistency rule). -/ +def CONSISTENCY_WIDTH : ℕ := 6 + +theorem layout_sum : 3 * LAYER_WIDTH + CONSISTENCY_WIDTH = DNA_LEN := by decide + +-- ============================================================ +-- §2 LAYOUT TYPE +-- ============================================================ + +/-- A valid Φ-encoded DNA sequence. + The only structural invariant is Layer 4: bases 24-29 are binary + (G = rule passed, T = rule failed). Layers 1-3 are unrestricted. -/ +structure PhiLayout where + seq : Fin 30 → HachimojiBase + h_layer4 : ∀ i : Fin 6, + seq ⟨24 + i.val, by omega⟩ = G ∨ + seq ⟨24 + i.val, by omega⟩ = T + +-- ============================================================ +-- §3 WINDOW SELECTORS +-- ============================================================ + +/-- Layer 1: F(E) byte-class frequencies (bases 0-7). -/ +def PhiLayout.layer1 (d : PhiLayout) : Fin 8 → HachimojiBase := + fun i => d.seq ⟨i.val, by omega⟩ + +/-- Layer 2: τ(E) AST node-type frequencies (bases 8-15). -/ +def PhiLayout.layer2 (d : PhiLayout) : Fin 8 → HachimojiBase := + fun i => d.seq ⟨8 + i.val, by omega⟩ + +/-- Layer 3: δ(E) child-ordering frequencies (bases 16-23). -/ +def PhiLayout.layer3 (d : PhiLayout) : Fin 8 → HachimojiBase := + fun i => d.seq ⟨16 + i.val, by omega⟩ + +/-- Layer 4: consistency rule pass/fail (bases 24-29). -/ +def PhiLayout.layer4 (d : PhiLayout) : Fin 6 → HachimojiBase := + fun i => d.seq ⟨24 + i.val, by omega⟩ + +-- ============================================================ +-- §4 PARTITION LEMMAS +-- ============================================================ + +/-- Every DNA position belongs to exactly one layer. -/ +theorem layer_partition (i : Fin 30) : + i.val < 8 ∨ (8 ≤ i.val ∧ i.val < 16) ∨ + (16 ≤ i.val ∧ i.val < 24) ∨ (24 ≤ i.val) := by omega + +/-- Layer selectors correspond to the right slice of seq. -/ +@[simp] theorem layer1_val (d : PhiLayout) (i : Fin 8) : + d.layer1 i = d.seq ⟨i.val, by omega⟩ := rfl + +@[simp] theorem layer2_val (d : PhiLayout) (i : Fin 8) : + d.layer2 i = d.seq ⟨8 + i.val, by omega⟩ := rfl + +@[simp] theorem layer3_val (d : PhiLayout) (i : Fin 8) : + d.layer3 i = d.seq ⟨16 + i.val, by omega⟩ := rfl + +@[simp] theorem layer4_val (d : PhiLayout) (i : Fin 6) : + d.layer4 i = d.seq ⟨24 + i.val, by omega⟩ := rfl + +-- ============================================================ +-- §5 LAYER 4 BINARY CONSTRAINT +-- ============================================================ + +/-- Layer 4 bases are binary: only G (pass) or T (fail). -/ +theorem layer4_binary (d : PhiLayout) (i : Fin 6) : + d.layer4 i = G ∨ d.layer4 i = T := d.h_layer4 i + +/-- Layer 4 never contains A, B, C, P, S, or Z. -/ +theorem layer4_not_ABCPSZ (d : PhiLayout) (i : Fin 6) : + d.layer4 i ≠ A ∧ d.layer4 i ≠ B ∧ d.layer4 i ≠ C ∧ + d.layer4 i ≠ P ∧ d.layer4 i ≠ S ∧ d.layer4 i ≠ Z := by + obtain (h | h) := layer4_binary d i <;> rw [h] <;> decide + +-- ============================================================ +-- §6 CONNECTION TO RING 2 (CharClass) +-- ============================================================ + +/-- The char class encoded at Layer 1 slot i. -/ +def layer1CharClass (d : PhiLayout) (i : Fin 8) : PhiCharClass := + baseToCharClass (d.layer1 i) + +/-- Roundtrip: the HachimojiBase at slot i is the base for char class i. -/ +theorem layer1_charclass_roundtrip (d : PhiLayout) (i : Fin 8) : + charClassToBase (layer1CharClass d i) = d.layer1 i := + base_charclass_roundtrip (d.layer1 i) + +-- ============================================================ +-- §7 SIMPLE CONSTRUCTOR (for witnesses) +-- ============================================================ + +/-- Build a PhiLayout from four function arguments. + Layer 4: con i = true → G (pass), false → T (fail). -/ +def mkPhiLayout + (f : Fin 8 → HachimojiBase) + (tau : Fin 8 → HachimojiBase) + (del : Fin 8 → HachimojiBase) + (con : Fin 6 → Bool) : PhiLayout where + seq := fun ⟨n, hn⟩ => + if h1 : n < 8 then f ⟨n, h1⟩ + else if h2 : n < 16 then tau ⟨n - 8, by omega⟩ + else if h3 : n < 24 then del ⟨n - 16, by omega⟩ + else if con ⟨n - 24, by omega⟩ then G else T + h_layer4 := by + intro ⟨j, hj⟩ + have h1 : ¬(24 + j < 8) := by omega + have h2 : ¬(24 + j < 16) := by omega + have h3 : ¬(24 + j < 24) := by omega + simp only [dif_neg h1, dif_neg h2, dif_neg h3] + split_ifs with _h + · exact Or.inl rfl + · exact Or.inr rfl + +end SilverSight.PhiDNALayout diff --git a/formal/SilverSight/PhiPipelineReceipt.lean b/formal/SilverSight/PhiPipelineReceipt.lean new file mode 100644 index 00000000..1b8b0412 --- /dev/null +++ b/formal/SilverSight/PhiPipelineReceipt.lean @@ -0,0 +1,154 @@ +/- +PhiPipelineReceipt.lean — Ring 5: pipeline receipt + +This ring closes the outward dependency spiral by connecting: + • Ring 3 (PhiDNALayout / mkPhiLayout) — the constructor + • Ring 4 (PhiConsistency) — the ADMIT/QUARANTINE predicates + +Core theorem: a layout built with consistency vector `con : Fin 6 → Bool` is +ADMITted if and only if every entry of `con` is `true`. + + isAdmit (mkPhiLayout f τ del con) ↔ ∀ i : Fin 6, con i = true + +This is the formal receipt: knowing `con` is sufficient to read the admission +decision without inspecting the full 30-base sequence. + +Anti-drift: any change to the slot mapping, to the G/T encoding, or to the +8+8+8+6 layout partition breaks this theorem before it reaches the user. +-/ + +import SilverSight.PhiConsistency +import Mathlib.Tactic + +namespace SilverSight.PhiPipelineReceipt + +open HachimojiBase +open SilverSight.PhiDNALayout +open SilverSight.PhiConsistency + +-- ============================================================ +-- §1 KEY LEMMA: Layer 4 evaluates to encodeRule (con i) +-- ============================================================ + +/-- For any layout built by mkPhiLayout, the base at Layer 4 slot i + is exactly encodeRule (con i) — G if the rule passed, T if not. -/ +lemma mkPhiLayout_layer4 (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) + (i : Fin 6) : + (mkPhiLayout f τ del con).layer4 i = encodeRule (con i) := by + have hi : i.val < 6 := i.isLt + simp only [PhiLayout.layer4, mkPhiLayout, encodeRule] + have h1 : ¬(24 + i.val < 8) := by omega + have h2 : ¬(24 + i.val < 16) := by omega + have h3 : ¬(24 + i.val < 24) := by omega + simp only [dif_neg h1, dif_neg h2, dif_neg h3] + have hval : 24 + i.val - 24 = i.val := by omega + simp only [hval, Fin.eta] + +-- ============================================================ +-- §2 SLOT SURJECTIVITY (and equivalence) +-- ============================================================ + +/-- Every Fin 6 slot is occupied by exactly one ConsistencyRule. -/ +theorem slot_surjective : Function.Surjective ConsistencyRule.slot := by + intro i + fin_cases i <;> + first + | exact ⟨.balanced_parens, rfl⟩ + | exact ⟨.valid_operator_order, rfl⟩ + | exact ⟨.valid_variable_name, rfl⟩ + | exact ⟨.no_empty_expression, rfl⟩ + | exact ⟨.single_expression, rfl⟩ + | exact ⟨.defined_reference, rfl⟩ + +/-- slot is a bijection between ConsistencyRule and Fin 6. -/ +noncomputable def slotEquiv : ConsistencyRule ≃ Fin 6 where + toFun := ConsistencyRule.slot + invFun := fun i => (slot_surjective i).choose + left_inv := fun r => slot_injective (slot_surjective r.slot).choose_spec + right_inv := fun i => (slot_surjective i).choose_spec + +-- ============================================================ +-- §3 ADMIT IFF (rule form) +-- ============================================================ + +/-- ADMIT ↔ every rule passes (in terms of ConsistencyRule). -/ +theorem mkPhiLayout_isAdmit_iff_rules + (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) : + isAdmit (mkPhiLayout f τ del con) ↔ + ∀ r : ConsistencyRule, con r.slot = true := by + simp only [isAdmit, mkPhiLayout_layer4, encodeRule] + constructor + · intro h r + have hr := h r + cases h_con : con r.slot <;> simp_all + · intro h r + simp [h r] + +-- ============================================================ +-- §4 PIPELINE RECEIPT (index form) +-- ============================================================ + +/-- Pipeline admit receipt: ADMIT ↔ all 6 consistency booleans are true. -/ +theorem pipeline_admit_iff + (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) : + isAdmit (mkPhiLayout f τ del con) ↔ ∀ i : Fin 6, con i = true := by + rw [mkPhiLayout_isAdmit_iff_rules] + constructor + · intro h i + obtain ⟨r, hr⟩ := slot_surjective i + simpa [hr] using h r + · intro h r + exact h r.slot + +/-- Pipeline quarantine receipt: QUARANTINE ↔ some consistency boolean is false. -/ +theorem pipeline_quarantine_iff + (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) : + isQuarantine (mkPhiLayout f τ del con) ↔ ∃ i : Fin 6, con i = false := by + simp only [isQuarantine, mkPhiLayout_layer4, encodeRule] + constructor + · intro ⟨r, hr⟩ + exact ⟨r.slot, by cases h : con r.slot <;> simp_all⟩ + · intro ⟨i, hi⟩ + obtain ⟨r, hr⟩ := slot_surjective i + exact ⟨r, by simp [hr, hi]⟩ + +-- ============================================================ +-- §5 COMPLEMENTARITY +-- ============================================================ + +/-- For mkPhiLayout: ADMIT ↔ NOT QUARANTINE. -/ +theorem pipeline_admit_iff_not_quarantine + (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) : + isAdmit (mkPhiLayout f τ del con) ↔ + ¬isQuarantine (mkPhiLayout f τ del con) := by + rw [pipeline_admit_iff, pipeline_quarantine_iff] + constructor + · intro hall ⟨i, hi⟩ + exact absurd hi (by simp [hall i]) + · intro hnone i + rcases Bool.eq_false_or_eq_true (con i) with h | h + · exfalso; exact hnone ⟨i, h⟩ + · exact h + +-- ============================================================ +-- §6 DECISION PROCEDURE +-- ============================================================ + +/-- Computable admission check: AND all 6 consistency booleans. -/ +def decidePipeline (con : Fin 6 → Bool) : Bool := + con ⟨0, by omega⟩ && con ⟨1, by omega⟩ && con ⟨2, by omega⟩ && + con ⟨3, by omega⟩ && con ⟨4, by omega⟩ && con ⟨5, by omega⟩ + +theorem decidePipeline_correct + (f τ del : Fin 8 → HachimojiBase) (con : Fin 6 → Bool) : + isAdmit (mkPhiLayout f τ del con) ↔ decidePipeline con = true := by + rw [pipeline_admit_iff] + simp only [decidePipeline, Bool.and_eq_true] + constructor + · intro h + exact ⟨⟨⟨⟨⟨h ⟨0, by omega⟩, h ⟨1, by omega⟩⟩, h ⟨2, by omega⟩⟩, + h ⟨3, by omega⟩⟩, h ⟨4, by omega⟩⟩, h ⟨5, by omega⟩⟩ + · intro ⟨⟨⟨⟨⟨h0, h1⟩, h2⟩, h3⟩, h4⟩, h5⟩ i + fin_cases i <;> assumption + +end SilverSight.PhiPipelineReceipt