# Typed mathematical dependency guide

The proof chapters are Julia strings in `src/ProofGuide.jl`, exported to `PROOFS.md`. The exact source declarations and individual arguments are indexed in `THEOREMS.toml` and `THEOREM_GUIDE.md`.

| Stage | Type | Dependencies and retained hypotheses | Proof / Julia support |
|---|---|---|---|
| Positive golden root, one-arcsecond angle, positive scale | Inputs and definitions | Usual real square root and circle constant; `a>0` for positive geometry | P01; `ExactArithmetic.jl` |
| Six labeled marks, major arc, outward segment images | Construction definitions | Placement convention, ordered levels and parametric intervals | P02; `Geometry.jl` |
| Endpoints, ordered levels, reflection, uniqueness under labeled coordinates | Derived set and coordinate identities | The construction definitions; some identities allow all real `a` | P02; polynomial identities and analytic set arguments |
| Average of both outer lengths; opposite semicircle length | Selected observables | Explicit selection rule; semicircle and both segments belong to the outline | P02 |
| `G=a*phi`, `C=a*pi`, `W=a*(phi+pi)` | Derived measurements | Positive radius, distance formula, derivative and speed integral | P01–P02; analytic proof and exact algebra |
| `lambda=G/W`, `mu=C/W` | Normalization and cancellation | `W>0`; selection precedes normalization | P01–P02; exact rational enclosure |
| Placed measurements | Metric invariance | Arbitrary center and real linear isometric embedding | P03; analytic proof; rational frames are computable examples |
| Affine dimension one; centered and Gram ranks two | Linear and affine consequences | Two distinct marks and two independent center-relative seed vectors when `a>0` | P04; exact moment and minor polynomials; rank-nullity proof |
| Radii, dot products, angle cosine, seed angle, triangle area | Derived Euclidean metrics | Positivity where norms are canceled; triangle identity permits every real `a` | P05; algebra plus analytic angle argument |
| Weighted mean and centered homothety observation | Algebraic identity and commuting observation | Positive mean denominator; real module; observation intercept one, or explicit intercept defect | P06; exact cleared polynomial identities and induction |
| Real-time homothety composition | Analytic implication | `lambda>0`; real powers through exponential and logarithm | P06; written proof |
| Grid quantizer and displacement coordinate `y=h*d` | Definition and coordinate interface | Independently retained `h>0`; signed integer coordinate identity | P06, P10; exact rational realization checks |
| `Q`, `S`, quotient and rational remainder | Definitions and Euclidean identities | Natural canonical state; generic ledger has separately stated signed domains | P07, P09; `Dynamics.jl` |
| Exact parameter interval `[4196/12343,7039/20706)` | Analytic finite-domain equality | Entire domain `0<=d<32768`; determinant-one boundary argument | P07; also exhaustive intersection of rational constraints |
| Rational lambda enclosure and remainder gap | Analytic bounds plus exhaustive finite certificate | Exact Machin bounds and integer square root; all 128×256 states checked | P01, P11; `ExactArithmetic.jl`, `Verification.jl` |
| Real-lambda and rational floor equality | Implication on a finite domain | Either exact interval argument or enclosure-plus-gap argument | P07 or P11 |
| Equality of finite trajectories | Induction using forward invariance | Initial state in `D`; any natural iteration depth | P07, P10; all 23-step records additionally checked |
| Precision threshold for every natural `p` | Analytic implication from monotonicity | `q_7<L<=q_8`, `q_p<=lambda<U` | P08; exact truncation and finite sweep support |
| Terminal state and ordered remainder list | Information-preserving encoding | Nonzero multiplier for unique recovery; positive divisor for canonical admissibility theorem | P09; reverse-step divisibility, bounds and signed ledger tests |
| Single canonical remainder below `S/2` | Domain-restricted modular encoding | Proven inverse of `Q/2` modulo `S/2`; seed bound retained | P11; exact inverse identity and domain-wide decoding |
| Extinction thresholds | Universal recurrence and induction | Natural states; `0<Q<S`; ceiling recurrence | P12; exact threshold list and state census |
| Geometric realization of recovered integers | Substitution requiring additional data | Scale, center and frame retained; positive radius for positive provenance | P03, P10; exact symbolic curve descriptor |
| Combined central theorem | Conjunction of established interfaces | All hypotheses from the exact declaration in `Omega/Main.lean` | P13 |

## Data that cannot be dropped at an interface

1. The marked construction and selected measurement rule identify which lengths supply the shares. The unmarked outline alone is not asserted to determine a unique readout.
2. `W=G+C` retains its meaning as the reference sum. The full outline component length is `a*(2*pi-epsilon)+2*a*phi^2`, which is larger.
3. Centered observations retain the intercept convention. For intercept `b`, the defect is exactly `(1-k)*(b-1)`.
4. Repeated quantization retains the rounding at each step. Two steps from 26 produce 2; one floor after multiplication by `lambda^2` produces 3.
5. Equality of successors retains the parameter type: `rho/S=q*d-F(d)`, while the real residual is `rho/S+(lambda-q)*d` on `D`.
6. General ledger decoding retains the terminal state and the **order** of the remainders, with every reverse step admissible. The full-period single-remainder result is a separate, restricted decoding theorem.
7. A reconstructed integer does not supply the geometric scale, center, or frame. Those are explicit realization inputs. Radius zero records termination; the positive-radius provenance theorem is invoked only with its positivity hypothesis.