# OMEGA NAUGHT: Lean 4 formal proof

This project formalizes the complete central geometric-provenance theorem and its arithmetic and reconstruction interfaces. The main result is `Omega.central_provenance_theorem` in `Omega/Main.lean`. The source contains 147 named, proved theorems.

The construction and its selected measurement rule are explicit inputs. The conclusion is that this rule yields the stated scalar and connects to the stated finite arithmetic system. It does not assert uniqueness of the measurement rule among all possible measurements of an unmarked outline.

## Exact main result

Let

\[
\varphi=(1+\sqrt5)/2,\quad \varepsilon=\pi/648000,
\quad\delta=\varepsilon/2,\quad s=\sin\delta,\quad c=\cos\delta.
\]

In the Euclidean plane identified with the complex numbers, the marked points are
\(p(a,z)=ac+iaz\), with ordered levels

\[
z\in\bigl[-(\varphi^2+s),-(1+s),-s,s,1+s,\varphi^2+s\bigr].
\]

The outline is the radius-\(a\) circular arc with parameter interval
\([\delta,2\pi-\delta]\), together with the two specified outward segments.
The golden readout is the average of the two outer segment lengths. The circular readout is the length of the opposite semicircle, whose parameter interval is \([\pi/2,3\pi/2]\). Arc length is expressed by the standard integral of speed of the smooth circular parametrization; the major-arc parametrization is proved injective on its interval.

For every \(a>0\), every center, and every real linear isometric embedding of this plane into an ambient real normed space,

\[
G=a\varphi,\quad C=a\pi,\quad W=G+C=a(\varphi+\pi),
\qquad G/W=\lambda=\frac{\varphi}{\varphi+\pi},
\quad C/W=\mu=1-\lambda.
\]

The selected weighted mean is exactly

\[
\frac{Gx+C}{G+C}=1+\lambda(x-1)=T(x).
\]

With \(Q=339949771344778\), \(S=10^{15}\), \(q=Q/S\),
\(D=\{0,\ldots,32767\}\), and \(F(d)=\lfloor Qd/S\rfloor\),

\[
\lfloor\lambda d\rfloor=F(d)\quad(d\in D).
\]

For every independently retained grid scale \(h>0\), every \(n\in\mathbb N\), and \(d\in D\), repeating the operation
\(y\mapsto h\lfloor\lambda y/h\rfloor\) gives exactly \(hF^{[n]}(d)\).

For the integer Euclidean ledger, every generated terminal state and ordered remainder list reconstructs its initial state and hence its entire trajectory. Conversely, the explicitly defined admissibility conditions characterize the ledgers of unique initial integer states. With a retained grid scale, center and isometric frame, this reconstructs the corresponding radius-requantized geometric object.

## Stronger exact results included

* `exact_parameter_interval`: for **every real** \(r\), its entire floor table on \(D\) equals the canonical table if and only if
  \[
  4196/12343\le r<7039/20706.
  \]
* `precision_threshold`: among decimal truncations \(q_p=\lfloor10^p\lambda\rfloor/10^p\), for **all natural** \(p\), agreement on the whole domain holds exactly when \(p\ge8\).
* `first_remainder_reconstruction`: one canonical remainder identifies each seed below the full period \(S/2=500000000000000\), which includes \(D\). The modular inverse is proved, not assumed.
* `finite_gap_certificate` and `certified_gap`: a kernel-reduced certificate covers all 32,768 states and proves \(S-\rho(d)\ge34535026732\). Equality is checked at \(d=20706\).
* `extinction_threshold`: a universal recurrence characterizes exactly when an iterate is zero. The thresholds through step ten are proved to be
  \(1,3,9,27,80,236,695,2045,6016,17697,52058\).
  Every seed in \(D\) reaches zero by step ten; precisely seeds 17697 through 32767 need that tenth step.
* The six marks have affine dimension one. Adjoining the center gives affine dimension two. Their center-relative span and Gram matrix have rank two. Injective linear embeddings preserve the span dimension.
* Euclidean radii, general pair distances, inner products, angle cosines, the exact seed angle and triangle areas are proved. The general formulas cover all fifteen mark pairs.

## Build

Pinned versions:

* Lean **4.19.0**, official release commit `6caaee842e94`.
* Mathlib **v4.19.0**, commit `c44e0c8ee63ca166450922a373c7409c5d26b00b`.
* `lake-manifest.json` pins the transitive package revisions.

With [Lean/Elan installed](https://lean-lang.org/install/), in this directory:

```bash
lake update
lake exe cache get
lake build
lake env lean Omega/AxiomAudit.lean
```

The default build checks `Omega.lean`, which imports the complete theorem chain through `Omega.Main`. `Omega/AxiomAudit.lean` separately reports the transitive axioms of every project theorem. `scripts/verify.sh` runs the build and checks that report. The compiler, dependencies and Mathlib cache are not bundled; initial setup needs network access. No `native_decide`, `sorry`, `admit`, or project-specific axioms are used in the proof source.

The ordinary foundational dependencies reported are `propext`, `Classical.choice`, and `Quot.sound`; some arithmetic results use fewer or none. This is a conventional Lean/Mathlib formalization, not an assertion that classical real mathematics is axiom-free.

## Read the proof

Start with `Omega/Main.lean`, then follow the imports. `PROOF_GUIDE.md` gives the mathematical argument and a typed dependency table. `SOURCE_MAPPING.md` states the translation conventions and exact scope. `REPRODUCTION.md` records the actual build environment and commands, including a container-specific executable-location shim needed in this session. `evidence/` contains the successful build and axiom reports.

The statistical workbook, codec benchmarks, timing observations and earlier Python execution histories are not converted into Lean theorems by this package. Likewise, some auxiliary manuscript presentation formulas, such as the individual arctangent bearing simplifications, are outside this formalization. These omissions do not supply hypotheses to the central proof: every dependency of the central Lean theorem is present or comes from the pinned Lean/Mathlib libraries.