Written proofs · Lean source · exact certificates

Proofs and code

Navigator for 147 indexed statements, Lean selected-measurement source, and the Julia proof companion. Written proofs, exact certificates, recorded executions. Not an additional source paper and not a joining theorem.

Main Lean result: Omega.central_provenance_theorem in Omega/Main.lean. Inputs: the marked construction and the selected measurements $G=a\varphi$ , $C=a\pi$ . Conclusion: those measurements yield $\lambda=\varphi/\Omega_0=G/W_{\mathrm{readout}}$ and connect to the certified floor and ledger maps.

Three entry points: read the mathematical proofs, inspect the exact certificates, run the reproduction.

Lean 4 source

Package omega_provenance v0.1. Hosted sources match SHA256SUMS. Python axiom-coverage PASS. lake build PASS on this archive 2026-09-13.

Julia companion

68 members, 147 declarations, 29 Lean reference files. Author-supplied O0/O3 records are not a site run. Distinct from the geometry plotting script.

Explicit ten-sample decoder

Written reconstruction of $\mathcal H_{\le 2}\oplus\mathbb R J$ from nine specified icosahedral samples and one extra value. Exact checker: 13 groups PASS. Not an additional source paper. The written note is the hosted Markdown file.

600-cell joint witness

Written argument that the next state and 120 residues modulo 8 determine an integer vector. 360 bits, with graph and order stored separately. The 306-bit counting bound is for the unbounded domain. Not a Lean proof and not a review of the written argument.

Exact field interface

Golden field inside $\mathbb Q(\sqrt2,\sqrt3,\sqrt5)$ . Eight rational coefficients, two norms, one rational reflection, and the split between injective samples and encoded records. Exact checker: 29 groups PASS. Not an additional source paper.

paper 8 Proof Audit 01

Localized forced flow, Theorems 7.3–7.6 and 8.6. Independent SymPy checks 29 PASS on this archive. Not peer review. Original TEX and original log were not supplied.

147 indexed statements

Each row is one named Lean declaration. Written proof chapters are in PROOFS.md and THEOREM_GUIDE.md. This navigator does not kernel-check Lean and does not run Julia.

SearchModuleChapter

Showing 147 of 147.

Statement

theorem central_provenance_theorem
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a h : ℝ) (ha : 0 < a) (hh : 0 < h) :
    (placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧
      placedG α E a/(placedG α E a+placedC α E a)=lam) ∧
    (∀ x : ℝ, (G a*x+C a)/(G a+C a)=T x) ∧
    (∀ d : ℕ, d < domainSize → Int.floor (lam*d)=(F d:ℤ)) ∧
    (∀ n d : ℕ, d < domainSize →
      (quantizedStep h)^[n] (h*d)=h*(F^[n] d:ℝ)) ∧
    (∀ n : ℕ, ∀ d : ℤ,
      Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2=d) ∧
    (∀ t : ℤ, ∀ rs : List ℤ, Ledger.Admissible Q S t rs ↔
      ∃! d : ℤ, Ledger.encode Q S rs.length d=(t,rs))

Hypotheses / context. No section-level variable declarations before this theorem; see the exact declaration and module definitions.

Proof step. Conjoin placed geometric provenance, weighted_mean, certified_floor_equality, grid_trajectory, specialized ledger roundtrip and admissibility_iff with their stated domains; no new inference from shape alone is inserted.

Evidence. Analytic composition of the typed theorem chain; it is not represented as a single Julia proof object.

Lean: reference/Lean/Omega/Main.lean:13 · Julia theorem guide · chapter P13