# Source mapping and scope

The formalization follows the supplied geometric-provenance manuscript and the completed independent audit. Earlier papers named in those documents are not imported as evidence or assumed theorems. The mathematical statements in the Lean files stand on their displayed definitions and the pinned Lean/Mathlib dependencies.

| Supplied material | Formal treatment |
|---|---|
| Manuscript constants and one-arcsecond seed | Explicit real definitions, quadratic identity, seed angle and arcsecond conversion |
| Six ordered marks and sequential bilateral extensions | Same coordinates and order; substitution, strict ordering, reflection and metric proofs |
| Construction-to-kernel characterization | Explicit component sets, endpoints, coordinate uniqueness and no retracing; all placements represented by a center and linear isometric frame |
| Golden measurement definition | The original **average of both outer lengths** is retained |
| Circular measurement definition | Opposite semicircle contained in the retained arc; smooth arc length represented by the integral of speed |
| Reference sum versus outline length | Separate definitions and a proved strict inequality |
| Weighted mean, homothety, scalar observation | Explicit identities with the required centered intercept; the arbitrary-intercept error is proved |
| Dimension statements | Affine dimension 1; center adjoined dimension 2; centered span and Gram rank 2; embedding invariance |
| General distances, radii, angle cosines, areas | Euclidean formulas for arbitrary signed levels, hence covering all fifteen pairs; exact seed angle also proved |
| Rational real bounds | Mathlib's proved 20-decimal π bounds and a proved golden-root enclosure replace the original Machin/enclosure implementation as the proof route |
| Finite certificate | Exact 32,768-state remainder-gap certificate reduced by Lean's ordinary decision procedure and converted into a universal inequality |
| Strongest audited floor theorem | Exact half-open interval of every real parameter giving the full table; proved analytically with the determinant argument |
| Decimal precision | Proved for every natural precision, extending the finite experimental sweep as an explicitly stronger theorem |
| Repeated quantization | One-step interface, invariant domain and arbitrary finite trajectories; checked counterexample to rounding just once |
| Ordered ledger | Generic integer theorem with all reverse admissibility conditions, uniqueness, whole-trajectory reconstruction and recursive positional polynomial identity |
| Rational versus real residual | Exact difference formula, strictly positive at positive seeds |
| Frozen SRSD v1.0 | Only the supplied scalar quotient-residual interface and its external arithmetic factorization are used |
| Geometric reconstruction | Retained scale, center and isometric frame are explicit arguments |
| Single-remainder identification | GCD, modular inverse and reconstruction below the full period are proved |
| Extinction thresholds | Universal recurrence and exact thresholds through step ten |

The complete **central theorem chain** is formalized. This is not a claim that every sentence, implementation, or auxiliary table in the supplied collection has been formalized. Specifically, this release does not formalize the statistical workbook and codec implementation; execution-time measurements; all individual arctangent bearing simplifications; the original Machin-series proof route; or the ambient-basis-extension theorem converting an isometry between framed planes into an isometry of an entire fixed finite-dimensional ambient space. The formal placement theorem instead quantifies directly over every real linear isometric embedding. These auxiliary statements are not assumptions of the central Lean theorem.

Lean's complex plane is a real Euclidean plane, not the coordinate product equipped with its maximum norm. `Module.finrank` is applied to the stated affine direction or linear span, never substituted for the ambient dimension. `arcLength` is explicitly the smooth parametrized-length integral; no formal equivalence to a separately defined Hausdorff measure or variation-based length is claimed.

No original constants, frozen interfaces or project definitions were altered to make a proof pass. The proof routes and representation choices listed above are explicit. The unchanged canonical quotient is Q/S, even though other parameters have the same finite floor table.