# Mathematical proof and dependency guide

All names below are in namespace `Omega`, except the generic integer ledger results in `Omega.Ledger`. The executable Lean source is the authoritative statement, including domains and hypotheses.

## 1. Constants and marked geometry

`Constants.lean` defines the positive golden root, the arcsecond angle and the normalized shares. Squaring the defining expression proves \(\varphi^2=\varphi+1\). The seed satisfies \(0<\delta<\pi/2\), so \(s,c>0\) and \(s^2+c^2=1\). Multiplying \(\varepsilon\) by \((180/\pi)3600\) gives exactly one arcsecond.

`Geometry.lean` specifies the actual circular parametrization and outward segments as sets. Substitution proves both seed endpoints, and the sequential extension equations yield the six specified marks. Their levels are strictly ordered. Reflection exchanges the two sides. Given their labeled real and imaginary coordinates, the marks are unique. The retained arc is injectively parametrized, so it does not retrace itself.

The difference of two marks is \(ia(z-w)\), whose Euclidean norm is \(a|z-w|\) for \(a>0\). Thus each inner extension has length \(a\), each outer extension has length \(a\varphi\), and each complete extension has length \(a\varphi^2\). Both outer lengths are used in the defined average \(G\).

The derivative of the circular parametrization has norm \(a\). Its speed integral over an interval \([u,v]\) is therefore \(a(v-u)\). The opposite semicircle interval is contained in the retained major interval, so its length is \(C=a\pi\). These are measurements of components belonging to the specified construction. They yield \(W=a(\varphi+\pi)\) and the normalized shares by cancellation of \(a>0\).

The total outline component length instead equals
\[
a(2\pi-\varepsilon)+2a\varphi^2.
\]
It is strictly larger than \(W\). The proof never identifies the two quantities.

`Placement.lean` transports the construction by \(z\mapsto\alpha+E(z)\), with \(E\) a real linear isometric embedding. Distances and the circular speed integral are unchanged. Positive scaling scales the outline and readouts as stated. These theorems cover translations, orientations and embeddings without assuming that the integer ledger contains a center or a frame.

## 2. Affine and homothety interfaces

In `Affine.lean`, direct algebra proves
\[
\frac{a\varphi x+a\pi}{a\varphi+a\pi}=1+\lambda(x-1).
\]
Its displacement from 1 is \(\lambda(x-1)\), and induction gives
\(T^{[n]}(x)=1+\lambda^n(x-1)\).

For a real module, define \(H_k(z)=\alpha+k(z-\alpha)\). Then
\(H_kH_l=H_{kl}\). Every real linear observation in the required centered form
\(v_L(z)=1+L(z-\alpha)\) satisfies
\(v_L(H_kz)=1+k(v_L(z)-1)\).
No injectivity of \(L\) is claimed. For an arbitrary intercept \(b\), the failure of this centered interface is exactly \((1-k)(b-1)\); hence the intercept condition is explicit. The real-time law uses positivity of \(\lambda\) and Mathlib's real-power addition theorem.

The Euclidean dimension statements in `Dimension.lean` distinguish the affine span of the marks from their linear span relative to the center. The former is a line containing two distinct marks. Two seed vectors linearly generate the whole plane: `seed_linear_combination` displays coefficients reconstructing any complex vector. The real dimension of that plane is two. The coordinate matrix has a positive diagonal two-by-two moment matrix and rank two. Mathlib's proved equality of the ranks of \(X\) and \(X^T X\) gives the Gram rank. No ambient dimension is inferred from these ranks.

## 3. The exact finite floor theorem

`Constants.lean` proves rational bounds on \(\varphi\) using its quadratic identity and positivity, and uses Mathlib's proved 20-decimal bounds on \(\pi\). Exact rational algebra yields
\[
q<\lambda<q+1/S.
\]
These are inequalities about real numbers with rational endpoints, not floating-point tests.

`Floor.lean` gives a stronger analytic proof of floor agreement. Set
\(L=4196/12343\), \(U=7039/20706\). Exact arithmetic verifies
\(L<q<U\) and \(L<\lambda<U\). Suppose an integer \(k\) satisfies
\(Ld<k<Ud\), for \(0\le d<32768\). The integers
\[
X=12343k-4196d,\quad Y=7039d-20706k
\]
are positive. The determinant identity
\(7039\cdot12343-4196\cdot20706=1\) gives
\[
d=20706X+12343Y\ge33049,
\]
a contradiction. Thus no integer boundary lies strictly between these multiples.

Euclidean division first identifies \(\lfloor qd\rfloor=F(d)\). For any \(L\le r<U\), if \(rd<F(d)\), then \(F(d)\) is a forbidden interior boundary. If \(F(d)+1\le rd\), then \(F(d)+1\) is a forbidden interior boundary. This proves the whole table agrees. Conversely, the floor constraints at \(d=12343\) and \(d=20706\) respectively require \(r\ge L\) and \(r<U\). This proves the exact half-open interval, including both endpoint conventions.

Separately, `Finite.lean` checks every state using a Boolean certificate divided into 128 blocks of 256 states. Ordinary Lean `decide` reduces the exact integer computations; its proof is checked by the kernel. `certified_gap` converts the Boolean statement into the universal inequality
\(S-\rho(d)\ge34535026732\), with equality at 20706. Since
\(S(\lambda-q)d<d\le32767<34535026732\), no rounding boundary can be crossed. This reproduces the finite-certificate route without trusting Python output.

## 4. Trajectories and precision

For positive integer \(d\), \(Q<S\) implies \(F(d)<d\); also \(F(0)=0\). Thus the finite domain is forward invariant. Induction extends one-step floor agreement to arbitrary finite trajectories.

For \(h>0\), substitution of \(y=hd\) in the floor quantizer gives
\(h\lfloor\lambda d\rfloor\). Combining this with the finite floor theorem and invariance proves the grid-trajectory theorem for every iteration depth. An explicitly checked counterexample is \(d=26\): two quantized steps yield 2, whereas \(\lfloor26\lambda^2\rfloor=3\).

Decimal truncations are monotone in their precision and bounded above by \(\lambda\). Exact real inequalities give \(q_7=3399497/10^7<L\) and \(q_8=33994977/10^8\ge L\). All truncations remain below \(U\). The exact parameter interval therefore proves agreement if and only if \(p\ge8\), including precisions beyond the original finite sweep.

`Extinction.lean` defines \(t_0=1\) and
\(t_{n+1}=\lceil St_n/Q\rceil=(St_n+Q-1)\mathbin{/}Q\) in natural-number division. The elementary equivalence \(F(d)<t\iff d<\lceil St/Q\rceil\), followed by induction, proves
\(F^{[n]}(d)=0\iff d<t_n\). The concrete threshold evaluations prove the tenth-step and deepest-seed statements.

## 5. Ordered reconstruction

`Ledger.lean` treats arbitrary integers with multiplier \(A\ne0\) and positive divisor \(B\); it does not assume the finite domain. Euclidean division gives
\[
Ad=Bd'+r,\quad 0\le r<B,
\qquad d=(Bd'+r)/A.
\]
Encoding retains the terminal state and the remainder list in forward order. Decoding consumes the list from the right. Induction proves exact roundtrip reconstruction.

Admissibility checks, at each reverse step, that the remainder is in \([0,B)\) and that \(Bd'+r\) is divisible by \(A\). From these conditions the recovered integer has exactly the prescribed quotient and remainder. Induction proves encoding the recovery returns precisely the proposed record. Combining this with roundtrip reconstruction proves that an admissible record is generated by exactly one initial integer. It also proves every later state is reconstructed.

The positional ledger value is defined recursively by
\[
V([])=0,\qquad V(r::rs)=A^{|rs|}r+B\,V(rs).
\]
Induction proves
\[
A^n d_0=B^n d_n+V([r_0,\ldots,r_{n-1}]).
\]
The displayed recurrence is the ordered polynomial
\(\sum_{j=0}^{n-1}B^jA^{n-1-j}r_j\): expanding the head gives its first term, and multiplying the tail by \(B\) gives exactly the remaining coefficients. The formal theorem uses this recursive polynomial definition.

Specializing \((A,B)=(Q,S)\) recovers the canonical dynamics. Independently, the proved modular inverse gives
\[
d=281419755786509\,(\rho(d)/2)\pmod{500000000000000}
\]
for all seeds below this period. This is the proved reason a single remainder is injective on the smaller audit domain; it does not replace the general ledger theorem.

## 6. Residual types and retained geometric data

`Interface.lean` proves the two-way scalar quotient-residual coordinate change, its canonical residual bounds, and the exact external factorization of \(Qd\). This is an application of the frozen external interface; it adds no SRSD algorithms or claims.

The rational normalized residual is \(\rho(d)/S=qd-F(d)\). The real-parameter residual is instead
\[
\lambda d-\lfloor\lambda d\rfloor
=\rho(d)/S+(\lambda-q)d.
\]
For positive \(d\), the correction is strictly positive. Equality of floor successors therefore does not identify the residuals.

`point_reconstruction` and `curve_reconstruction` explicitly consume retained scale, center and frame data. The ledger reconstructs integers. The retained data turn those integers into grid displacements, points or radius-requantized outlines. Positive radii remain a hypothesis when the geometric provenance result is invoked; radius zero denotes termination rather than a positive-radius construction.

## Typed dependency table

| Stage | Type | Lean location |
|---|---|---|
| Golden rule, arcsecond seed, positive scale, labeled marks and frame | Inputs and definitions | Constants, Geometry, Placement |
| Retained arc and bilateral segments | Defined sets, derived endpoint and length identities | Geometry |
| Mean of outer lengths and opposite semicircle | Selected observables | `G`, `C` |
| \(G=a\varphi,C=a\pi\), normalized shares | Derived real identities | `geometric_provenance`, `provenance_all_placements` |
| Weighted mean and homothety | Algebraic identity and commuting observation | Affine |
| Quantizer and independent grid scale | Definition and coordinate interface | Affine, Interface |
| Canonical rational arithmetic | Definitions and Euclidean identities | Floor |
| Exact table interval | Analytic finite-domain equality | `exact_parameter_interval` |
| Remainder gap | Exhaustive, kernel-checked finite certificate | Finite |
| Finite trajectories | Implication using forward invariance | `trajectory_equality`, `grid_trajectory` |
| Terminal state and ordered remainders | Information-preserving encoding with admissibility | Ledger |
| Scale, center, frame, positive radius | Additional realization data | Placement, Interface |
| Combined provenance theorem | Composition of the proved interfaces | Main |