# All 147 source theorems: declarations and proof steps

Every declaration below is copied verbatim from its supplied Lean module. Section variables and module definitions remain applicable; the source file is the authority for elaborated domains. The new mathematical proof is in `PROOFS.md` and the Julia string `PROOFS[chapter]`. Computational evidence does not replace the analytic argument.

## Omega.weighted_mean

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 11. Proof chapter: **P06**.

```lean
theorem weighted_mean (a x : ℝ) (ha : 0 < a) :
    (a * phi * x + a * Real.pi) / (a * phi + a * Real.pi) = T x
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Subtract one, factor a and cancel the positive denominator a(phi+pi).

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.displacement_conjugacy

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 20. Proof chapter: **P06**.

```lean
theorem displacement_conjugacy (x : ℝ) : T x - 1 = lam * (x - 1)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Expand T(x) and subtract one.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.affine_iterate

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 24. Proof chapter: **P06**.

```lean
theorem affine_iterate (n : ℕ) (x : ℝ) :
    T^[n] x = 1 + lam^n * (x - 1)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on natural n; the base is the identity and the step multiplies the centered displacement by lambda.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.homothety_comp

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 39. Proof chapter: **P06**.

```lean
theorem homothety_comp (k l : ℝ) (α z : V) :
    homothety k α (homothety l α z) = homothety (k*l) α z
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Expand both centered homotheties and apply the real-module distributive laws.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.homothety_one

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 43. Proof chapter: **P06**.

```lean
theorem homothety_one (α z : V) : homothety 1 α z = z
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Simplify alpha+1*(z-alpha).

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.observation_commutes

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 46. Proof chapter: **P06**.

```lean
theorem observation_commutes (L : V →ₗ[ℝ] ℝ) (k : ℝ) (α z : V) :
    observation L α (homothety k α z) = Tk k (observation L α z)
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Use real linearity of L on k*(z-alpha) and the fixed intercept one.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.observation_iterate

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 50. Proof chapter: **P06**.

```lean
theorem observation_iterate (L : V →ₗ[ℝ] ℝ) (n : ℕ) (α z : V) :
    observation L α (homothety (lam^n) α z) = T^[n] (observation L α z)
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Use observation_commutes at k=lambda^n and substitute the affine iterate formula.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.real_time_semigroup

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 55. Proof chapter: **P06**.

```lean
theorem real_time_semigroup (t u : ℝ) (α z : V) :
    homothety (lam^t) α (homothety (lam^u) α z) = homothety (lam^(t+u)) α z
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: For lambda>0 write lambda^t=exp(t log(lambda)); exponential addition gives the coefficient law, then use homothety_comp for all real times.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.arbitrary_intercept_defect

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 59. Proof chapter: **P06**.

```lean
theorem arbitrary_intercept_defect (L : V →ₗ[ℝ] ℝ) (k b : ℝ) (α z : V) :
    (b + L (homothety k α z - α)) - Tk k (b + L (z - α)) =
      (1-k)*(b-1)
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Expand the two observations and collect the difference (1-k)(b-1), explicitly retaining arbitrary b.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.grid_interface

Source: [reference/Lean/Omega/Affine.lean](reference/Lean/Omega/Affine.lean), line 68. Proof chapter: **P06**.

```lean
theorem grid_interface (h : ℝ) (hh : 0 < h) (d : ℤ) :
    quantizedStep h (h*d) = h * (Int.floor (lam*d) : ℝ)
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: For h>0 and any signed integer d, cancel h inside floor(lambda*(h*d)/h); this alone does not replace lambda by q.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.phi_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 24. Proof chapter: **P01**.

```lean
theorem phi_pos : 0 < phi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The nonnegative root sqrt(5) is positive, and (1+sqrt(5))/2 is positive.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.phi_sq

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 26. Proof chapter: **P01**.

```lean
theorem phi_sq : phi ^ 2 = phi + 1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Expand the defining expression and substitute sqrt(5)^2=5.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.phi_bounds

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 31. Proof chapter: **P01**.

```lean
theorem phi_bounds : 1.61803398874989484820 < phi ∧
    phi < 1.61803398874989484821
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Evaluate x^2-x-1 at the two exact decimal rationals and use its strict increase above 1/2 with the positive-root identity.

Evidence: Analytically justified exact rational enclosures, with all endpoint comparisons computed as Rational{BigInt}.

## Omega.denominator_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 37. Proof chapter: **P01**.

```lean
theorem denominator_pos : 0 < phi + Real.pi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Add phi>0 and pi>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.lam_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 39. Proof chapter: **P01**.

```lean
theorem lam_pos : 0 < lam
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Divide positive phi by positive phi+pi.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.lam_lt_one

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 41. Proof chapter: **P01**.

```lean
theorem lam_lt_one : lam < 1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The denominator exceeds phi because pi>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.shares_sum

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 46. Proof chapter: **P01**.

```lean
theorem shares_sum : lam + mu = 1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Combine fractions over the same nonzero denominator and cancel.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mu_eq_one_sub

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 50. Proof chapter: **P01**.

```lean
theorem mu_eq_one_sub : mu = 1 - lam
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Rearrange shares_sum.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.lam_bounds

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 52. Proof chapter: **P01**.

```lean
theorem lam_bounds : (339949771344778 : ℝ) / 10^15 < lam ∧
    lam < (339949771344779 : ℝ) / 10^15
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply monotonicity of f/(f+p) to exact phi and pi rational enclosures; check strict outer endpoints by cross multiplication.

Evidence: Analytically justified exact rational enclosures, with all endpoint comparisons computed as Rational{BigInt}.

## Omega.q_lt_lam

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 66. Proof chapter: **P01**.

```lean
theorem q_lt_lam : q < lam
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Identify the lower endpoint in lam_bounds with Q/S.

Evidence: Analytically justified exact rational enclosures, with all endpoint comparisons computed as Rational{BigInt}.

## Omega.lam_lt_q_plus

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 71. Proof chapter: **P01**.

```lean
theorem lam_lt_q_plus : lam < q + 1 / S
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Identify the upper endpoint in lam_bounds with q+1/S.

Evidence: Analytically justified exact rational enclosures, with all endpoint comparisons computed as Rational{BigInt}.

## Omega.delta_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 76. Proof chapter: **P01**.

```lean
theorem delta_pos : 0 < delta
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiply pi>0 by 1/1296000>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.delta_lt_half_pi

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 78. Proof chapter: **P01**.

```lean
theorem delta_lt_half_pi : delta < Real.pi / 2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compare the positive rational coefficients 1/1296000 and 1/2 of pi.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.s_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 82. Proof chapter: **P01**.

```lean
theorem s_pos : 0 < s
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use 0<delta<pi and the sign of sine on that interval.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.c_pos

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 86. Proof chapter: **P01**.

```lean
theorem c_pos : 0 < c
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use delta in (-pi/2,pi/2) and the sign of cosine.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.sc_identity

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 92. Proof chapter: **P01**.

```lean
theorem sc_identity : s ^ 2 + c ^ 2 = 1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Differentiate sin(t)^2+cos(t)^2, obtain zero, and evaluate at zero. Polynomial reduction subsequently uses this established identity.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.one_arcsecond

Source: [reference/Lean/Omega/Constants.lean](reference/Lean/Omega/Constants.lean), line 94. Proof chapter: **P01**.

```lean
theorem one_arcsecond : epsilon * (180 / Real.pi) * 3600 = 1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Cancel pi!=0 and evaluate 180*3600=648000.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.seeds_distinct

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 8. Proof chapter: **P04**.

```lean
theorem seeds_distinct (a : ℝ) (ha : 0 < a) : mark a s ≠ mark a (-s)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Their imaginary coordinates differ by 2as>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.marks_collinear

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 14. Proof chapter: **P04**.

```lean
theorem marks_collinear (a : ℝ) : Collinear ℝ (Set.range (marks a))
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Every mark equals (ac,0)+az(0,1); valid even for a=0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.marks_affine_dimension

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 21. Proof chapter: **P04**.

```lean
theorem marks_affine_dimension (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (affineSpan ℝ (Set.range (marks a))).direction=1
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Combine collinearity with two distinct seed marks; the direction is the span of their nonzero difference and has dimension one.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.seed_linear_combination

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 29. Proof chapter: **P04**.

```lean
theorem seed_linear_combination (a : ℝ) (ha : 0 < a) (z : ℂ) :
    ((z.re/(a*c)+z.im/(a*s))/2) • mark a s+
    ((z.re/(a*c)-z.im/(a*s))/2) • mark a (-s)=z
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use coefficients (x/(ac)+y/(as))/2 and (x/(ac)-y/(as))/2; verify both coordinates with ac,as nonzero.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.centered_span

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 41. Proof chapter: **P04**.

```lean
theorem centered_span (a : ℝ) (ha : 0 < a) :
    Submodule.span ℝ (Set.range (marks a))=⊤
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The explicit seed combination places every complex vector in the linear span of the marks.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.center_relative_rank

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 52. Proof chapter: **P04**.

```lean
theorem center_relative_rank (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (Submodule.span ℝ (Set.range (marks a)))=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The centered span is the whole complex plane, of real dimension two.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.center_adjoined_affine_dimension

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 56. Proof chapter: **P04**.

```lean
theorem center_adjoined_affine_dimension (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (affineSpan ℝ (insert 0 (Set.range (marks a)))).direction=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Adjoining zero makes affine direction the linear span of the marks; apply center_relative_rank.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.moment_matrix

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 73. Proof chapter: **P04**.

```lean
theorem moment_matrix (a : ℝ) :
    moment a=!![6*(a*c)^2,0;0,2*a^2*(s^2+(1+s)^2+(phi^2+s)^2)]
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Sum the six column outer products; paired levels cancel the off-diagonal entry. No a>0 hypothesis is needed for the equality.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.coordinates_rank

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 79. Proof chapter: **P04**.

```lean
theorem coordinates_rank (a : ℝ) (ha : 0 < a) : (coordinates a).rank=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The two diagonal entries of the moment matrix are positive for a>0; alternatively the seed minor is -2a^2cs!=0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.gram_rank

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 102. Proof chapter: **P04**.

```lean
theorem gram_rank (a : ℝ) (ha : 0 < a) : (gram a).rank=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The kernels of X and transpose(X)*X agree since v^T X^T X v=norm(Xv)^2; apply rank-nullity and coordinates_rank.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.gram_entries

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 105. Proof chapter: **P04**.

```lean
theorem gram_entries (a : ℝ) (i j : Fin 6) :
    gram a i j=a^2*(c^2+heights i*heights j)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiply the two coordinate rows to get a^2(c^2+z_i*z_j), for every real a and all 36 ordered entries.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.embedded_center_relative_rank

Source: [reference/Lean/Omega/Dimension.lean](reference/Lean/Omega/Dimension.lean), line 112. Proof chapter: **P04**.

```lean
theorem embedded_center_relative_rank {V : Type*} [AddCommGroup V] [Module ℝ V]
    (E : ℂ →ₗ[ℝ] V) (hE : Function.Injective E) (a : ℝ) (ha : 0 < a) :
    Module.finrank ℝ (Submodule.span ℝ (E '' Set.range (marks a)))=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: An injective linear E is an isomorphism onto its image on the span, preserving its real dimension two. No norm or ambient dimension restriction is introduced.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.step_threshold

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 9. Proof chapter: **P12**.

```lean
theorem step_threshold (d t : ℕ) : F d < t ↔ d < (S*t+Q-1)/Q
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For natural d,t, F(d)<t iff Qd<St iff d<ceil(St/Q); evaluate the ceiling by natural division (St+Q-1)/Q, including t=0.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.extinction_threshold

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 13. Proof chapter: **P12**.

```lean
theorem extinction_threshold (n d : ℕ) : F^[n] d=0 ↔ d < threshold n
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on n using t_0=1 and the step_threshold equivalence at t_n.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.threshold_values

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 20. Proof chapter: **P12**.

```lean
theorem threshold_values : (List.range 11).map threshold=
    [1,3,9,27,80,236,695,2045,6016,17697,52058]
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Evaluate the exact ceiling recurrence through depth ten, retaining the integer list.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.extinction_by_ten

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 23. Proof chapter: **P12**.

```lean
theorem extinction_by_ten (d : ℕ) (hd : d < domainSize) : F^[10] d=0
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The domain maximum 32767 is below t_10=52058, so apply extinction_threshold.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.deepest_seeds

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 30. Proof chapter: **P12**.

```lean
theorem deepest_seeds (d : ℕ) (hd : d < domainSize) :
    F^[9] d ≠ 0 ∧ F^[10] d=0 ↔ 17697 ≤ d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: At depth nine the state is nonzero exactly when d>=t_9=17697; all domain states are zero at depth ten.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.all_twenty_three_steps

Source: [reference/Lean/Omega/Extinction.lean](reference/Lean/Omega/Extinction.lean), line 39. Proof chapter: **P12**.

```lean
theorem all_twenty_three_steps (d : ℕ) (hd : d < domainSize) : F^[23] d=0
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compose extinction_by_ten with thirteen iterations of the absorbing fixed point F(0)=0.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.gcd_constants

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 9. Proof chapter: **P11**.

```lean
theorem gcd_constants : Nat.gcd Q S=2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use the exact Euclidean gcd algorithm on Q and S.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.inverse_identity

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 10. Proof chapter: **P11**.

```lean
theorem inverse_identity : halfQ*inverse=1+95668581631527*period
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Check (Q/2)*281419755786509=1+95668581631527*(S/2) by integer multiplication.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.remainder_halved

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 12. Proof chapter: **P11**.

```lean
theorem remainder_halved (d : ℕ) : rho d/2=(halfQ*d)%period
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Divide (Q/2)d by S/2; multiplying the Euclidean decomposition by two identifies rho(d) as twice that remainder.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.first_remainder_reconstruction

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 20. Proof chapter: **P11**.

```lean
theorem first_remainder_reconstruction (d : ℕ) (hd : d < period) :
    seedFromRemainder (rho d)=d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiply the halved-remainder congruence by the proved modular inverse and use 0<=d<S/2 to identify d mod (S/2) with d.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.first_remainder_injective

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 32. Proof chapter: **P11**.

```lean
theorem first_remainder_injective :
    Set.InjOn rho {d : ℕ | d < period}
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply first_remainder_reconstruction to equal remainders of seeds below S/2.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.first_remainder_injective_domain

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 39. Proof chapter: **P11**.

```lean
theorem first_remainder_injective_domain :
    Set.InjOn rho {d : ℕ | d < domainSize}
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: D is a subset of the full period [0,S/2); specialize first_remainder_injective.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.finite_gap_certificate

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 50. Proof chapter: **P11**.

```lean
theorem finite_gap_certificate :
    (List.range 128).all (fun b => (List.range 256).all
      (fun i => decide (34535026732 ≤ S-rho (256*b+i))))=true
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Check every state d=256b+i for all 128 blocks and 256 offsets using exact integer arithmetic. Julia verifies the same finite conjunction; it does not reproduce Lean's kernel trust mechanism.

Evidence: Exhaustive exact integer certificate over all 32,768 states, plus the block-coverage implication; checked by Julia/GMP, not Lean kernel.

## Omega.certified_gap

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 54. Proof chapter: **P11**.

```lean
theorem certified_gap (d : ℕ) (hd : d < domainSize) :
    34535026732 ≤ S-rho d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Each natural d<32768 has unique block b=d div 256 and offset i=d mod 256; specialize the complete finite conjunction.

Evidence: Exhaustive exact integer certificate over all 32,768 states, plus the block-coverage implication; checked by Julia/GMP, not Lean kernel.

## Omega.minimum_gap_attained

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 65. Proof chapter: **P11**.

```lean
theorem minimum_gap_attained : S-rho 20706=34535026732
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compute S-rho(20706)=34535026732 exactly and combine with the universal domain lower bound.

Evidence: Exhaustive exact integer certificate over all 32,768 states, plus the block-coverage implication; checked by Julia/GMP, not Lean kernel.

## Omega.finite_certificate_inequality

Source: [reference/Lean/Omega/Finite.lean](reference/Lean/Omega/Finite.lean), line 67. Proof chapter: **P11**.

```lean
theorem finite_certificate_inequality :
    (32767:ℕ)<34535026732
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compare the exact natural integers 32767 and 34535026732. P11.3 then uses this inequality in the complete real floor argument, handling d=0 explicitly.

Evidence: Exact integer identities and analytic implications; exhaustive computation is restricted to the explicitly finite certificate domain.

## Omega.S_pos

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 10. Proof chapter: **P07**.

```lean
theorem S_pos : 0 < S
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compare the exact integer S with zero.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.Q_pos

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 11. Proof chapter: **P07**.

```lean
theorem Q_pos : 0 < Q
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compare the exact integer Q with zero.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.Q_lt_S

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 12. Proof chapter: **P07**.

```lean
theorem Q_lt_S : Q < S
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compare the displayed exact integers.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.division_identity

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 14. Proof chapter: **P07**.

```lean
theorem division_identity (d : ℕ) : S*F d + rho d = Q*d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply natural Euclidean division to Q*d by positive S.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.remainder_bound

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 17. Proof chapter: **P07**.

```lean
theorem remainder_bound (d : ℕ) : rho d < S
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply the Euclidean remainder bound for positive S.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.step_zero

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 19. Proof chapter: **P07**.

```lean
theorem step_zero : F 0 = 0
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The quotient of zero by S is zero.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.step_lt

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 21. Proof chapter: **P07**.

```lean
theorem step_lt (d : ℕ) (hd : 0 < d) : F d < d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For positive d, Qd<Sd implies floor(Qd/S)<d.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.step_le

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 25. Proof chapter: **P07**.

```lean
theorem step_le (d : ℕ) : F d ≤ d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use step_lt when d>0 and step_zero when d=0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.forward_invariant

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 30. Proof chapter: **P07**.

```lean
theorem forward_invariant (d : ℕ) (hd : d < domainSize) : F d < domainSize
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Combine F(d)<=d with d<32768.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.step_monotone

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 33. Proof chapter: **P07**.

```lean
theorem step_monotone : Monotone F
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiplication by Q/S>0 and taking floors are monotone.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.q_in_interval

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 42. Proof chapter: **P07**.

```lean
theorem q_in_interval : lower < q ∧ q < upper
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Check L<q<U by exact rational cross multiplication.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.lam_in_interval

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 43. Proof chapter: **P07**.

```lean
theorem lam_in_interval : lower < lam ∧ lam < upper
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Place the proven rational enclosure for lambda strictly inside (L,U).

Evidence: Analytically justified exact rational enclosures, with all endpoint comparisons computed as Rational{BigInt}.

## Omega.floor_q

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 48. Proof chapter: **P07**.

```lean
theorem floor_q (d : ℕ) : Int.floor (q*d) = (F d : ℤ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Divide Qd=S F(d)+rho(d) by positive S and use 0<=rho<S to characterize the floor.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.no_interior_boundary

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 65. Proof chapter: **P07**.

```lean
theorem no_interior_boundary (d : ℕ) (hd : d < domainSize) (k : ℤ)
    (hl : lower*d < k) (hu : (k:ℝ) < upper*d) : False
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Form positive integers X=12343k-4196d and Y=7039d-20706k; determinant one gives d=20706X+12343Y>=33049, a contradiction.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.floor_agreement_of_interval

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 81. Proof chapter: **P07**.

```lean
theorem floor_agreement_of_interval (r : ℝ) (hr : lower ≤ r ∧ r < upper)
    (d : ℕ) (hd : d < domainSize) : Int.floor (r*d) = (F d:ℤ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For L<=r<U and d>0, either failed floor inequality creates a forbidden integer boundary. Handle d=0 directly.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.exact_parameter_interval

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 107. Proof chapter: **P07**.

```lean
theorem exact_parameter_interval (r : ℝ) :
    (∀ d : ℕ, d < domainSize → Int.floor (r*d) = (F d:ℤ)) ↔
      lower ≤ r ∧ r < upper
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The preceding implication gives sufficiency; seeds 12343 and 20706 force r>=L and r<U respectively.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.certified_floor_equality

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 120. Proof chapter: **P07**.

```lean
theorem certified_floor_equality (d : ℕ) (hd : d < domainSize) :
    Int.floor (lam*d) = (F d:ℤ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply floor_agreement_of_interval with lambda in (L,U).

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.trajectory_equality

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 126. Proof chapter: **P07**.

```lean
theorem trajectory_equality (r : ℝ) (hr : lower ≤ r ∧ r < upper)
    (n d : ℕ) (hd : d < domainSize) : (realStep r)^[n] d = F^[n] d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on every natural depth; one-step agreement and forward invariance keep each successor in D.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.truncation_le

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 139. Proof chapter: **P08**.

```lean
theorem truncation_le (p : ℕ) : truncation p ≤ lam
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: floor(10^p lambda)<=10^p lambda and the denominator is positive.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.truncation_succ

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 144. Proof chapter: **P08**.

```lean
theorem truncation_succ (p : ℕ) : truncation p ≤ truncation (p+1)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: If m=floor(10^p lambda), integer 10m<=10^(p+1)lambda, so 10m<=floor(10^(p+1)lambda).

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.truncation_monotone

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 159. Proof chapter: **P08**.

```lean
theorem truncation_monotone : Monotone truncation
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Iterate the successor inequality by induction for any two natural precisions in order.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.truncation_seven

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 161. Proof chapter: **P08**.

```lean
theorem truncation_seven : truncation 7 = 3399497/10000000
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The strict rational lambda enclosure fixes floor(10^7 lambda)=3399497.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.truncation_eight

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 169. Proof chapter: **P08**.

```lean
theorem truncation_eight : truncation 8 = 33994977/100000000
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The strict rational lambda enclosure fixes floor(10^8 lambda)=33994977.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.precision_threshold

Source: [reference/Lean/Omega/Floor.lean](reference/Lean/Omega/Floor.lean), line 178. Proof chapter: **P08**.

```lean
theorem precision_threshold (p : ℕ) :
    (∀ d : ℕ, d < domainSize → Int.floor (truncation p*d) = (F d:ℤ)) ↔ 8 ≤ p
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For p<8 monotonicity gives q_p<=q_7<L; for p>=8 it gives L<=q_8<=q_p<=lambda<U. Apply the exact parameter interval in both directions for every natural p.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.arc_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 24. Proof chapter: **P02**.

```lean
theorem arc_length (a u v : ℝ) (ha : 0 < a) : arcLength a u v=(v-u)*a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Differentiate gamma_a(t); for a>0 its speed is a. Integrate the constant on the oriented interval u..v. A length interpretation additionally uses u<=v.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.semicircle_retained

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 28. Proof chapter: **P02**.

```lean
theorem semicircle_retained (a : ℝ) : oppositeSemicircle a ⊆ majorArc a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The inequalities delta<pi/2 and 3pi/2<2pi-delta give parameter interval inclusion; apply image monotonicity for every real a.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.semicircle_in_outline

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 34. Proof chapter: **P02**.

```lean
theorem semicircle_in_outline (a : ℝ) : oppositeSemicircle a ⊆ outline a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compose semicircle_retained with the major-arc inclusion in the defining union.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.major_arc_no_retracing

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 38. Proof chapter: **P02**.

```lean
theorem major_arc_no_retracing (a : ℝ) (ha : 0 < a) :
    Set.InjOn (circleMap 0 a) (Icc delta (2*Real.pi-delta))
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For a>0 equal circle points have parameter difference in 2pi Z. Its absolute value is less than 2pi on the retained interval, so it is zero.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.upper_seed_endpoint

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 45. Proof chapter: **P02**.

```lean
theorem upper_seed_endpoint (a : ℝ) : circleMap 0 a delta=mark a s
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Evaluate cosine and sine at delta using c and s.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.lower_seed_endpoint

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 48. Proof chapter: **P02**.

```lean
theorem lower_seed_endpoint (a : ℝ) : circleMap 0 a (2*Real.pi-delta)=mark a (-s)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use periodicity and even cosine/odd sine at 2pi-delta.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_re

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 53. Proof chapter: **P02**.

```lean
theorem mark_re (a z : ℝ) : (mark a z).re=a*c
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Read the real component of ac+i az.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_im

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 54. Proof chapter: **P02**.

```lean
theorem mark_im (a z : ℝ) : (mark a z).im=a*z
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Read the imaginary component of ac+i az.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.bilateral_reflection

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 56. Proof chapter: **P02**.

```lean
theorem bilateral_reflection (a z : ℝ) : star (mark a z)=mark a (-z)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Complex conjugation fixes the real coordinate and negates az.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_distance

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 59. Proof chapter: **P02**.

```lean
theorem mark_distance (a z w : ℝ) (ha : 0 < a) :
    dist (mark a z) (mark a w)=a*|z-w|
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Subtract coordinates to obtain i a(z-w), then take the norm and use a>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.inner_extension_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 68. Proof chapter: **P02**.

```lean
theorem inner_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (1+s)) (mark a s)=a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Insert levels 1+s and s into mark_distance; the difference is 1.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.outer_extension_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 74. Proof chapter: **P02**.

```lean
theorem outer_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (phi^2+s)) (mark a (1+s))=a*phi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The level difference phi^2-1 equals positive phi.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.negative_outer_extension_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 80. Proof chapter: **P02**.

```lean
theorem negative_outer_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (-(phi^2+s))) (mark a (-(1+s)))=a*phi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The level difference is -phi, whose absolute value is phi.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.total_extension_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 86. Proof chapter: **P02**.

```lean
theorem total_extension_length (a : ℝ) (ha : 0 < a) :
    dist (mark a (phi^2+s)) (mark a s)=a*phi^2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The level difference is phi^2>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.chord_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 91. Proof chapter: **P02**.

```lean
theorem chord_length (a : ℝ) (ha : 0 < a) :
    dist (mark a s) (mark a (-s))=2*a*s
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The seed level difference is 2s>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.outer_segment_retained

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 96. Proof chapter: **P02**.

```lean
theorem outer_segment_retained (a : ℝ) :
    mark a '' Icc (1+s) (phi^2+s) ⊆ outline a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The upper outer level interval is contained in the full upper extension interval, hence in the outline union; no radius positivity is needed.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.G_eq

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 110. Proof chapter: **P02**.

```lean
theorem G_eq (a : ℝ) (ha : 0 < a) : G a=a*phi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Average both outer lengths, each a phi.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.C_eq

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 113. Proof chapter: **P02**.

```lean
theorem C_eq (a : ℝ) (ha : 0 < a) : C a=a*Real.pi
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply the constant-speed integral to [pi/2,3pi/2].

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.W_eq

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 117. Proof chapter: **P02**.

```lean
theorem W_eq (a : ℝ) (ha : 0 < a) : W a=a*(phi+Real.pi)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Add G_eq and C_eq and factor a.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.geometric_provenance

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 121. Proof chapter: **P02**.

```lean
theorem geometric_provenance (a : ℝ) (ha : 0 < a) :
    G a/W a=lam ∧ C a/W a=mu
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Cancel positive a from both normalized shares, using phi+pi>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.outline_length

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 130. Proof chapter: **P02**.

```lean
theorem outline_length (a : ℝ) (ha : 0 < a) :
    outlineLength a=a*(2*Real.pi-epsilon)+2*a*phi^2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Add the major-arc speed integral and both complete extension lengths; substitute 2delta=epsilon.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.reference_not_outline

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 139. Proof chapter: **P02**.

```lean
theorem reference_not_outline (a : ℝ) (ha : 0 < a) : W a < outlineLength a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Subtract W from outlineLength to obtain a(pi-epsilon+phi+2)>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.marked_coordinate_uniqueness

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 146. Proof chapter: **P02**.

```lean
theorem marked_coordinate_uniqueness (a : ℝ) (p : Fin 6 → ℂ)
    (hre : ∀ i, (p i).re=a*c) (him : ∀ i, (p i).im=a*heights i) : p=marks a
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For every label, equality of real and imaginary coordinates gives equality of complex points; use function extensionality.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.heights_strictly_ordered

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 153. Proof chapter: **P02**.

```lean
theorem heights_strictly_ordered : StrictMono heights
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Consecutive level gaps are phi,1,2s,1,phi, all positive.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.sequential_extensions

Source: [reference/Lean/Omega/Geometry.lean](reference/Lean/Omega/Geometry.lean), line 158. Proof chapter: **P02**.

```lean
theorem sequential_extensions (a : ℝ) :
    mark a s+(a:ℂ)*I=mark a (1+s) ∧
    mark a (1+s)+(a*phi:ℝ)*I=mark a (phi^2+s) ∧
    mark a (-s)-(a:ℂ)*I=mark a (-(1+s)) ∧
    mark a (-(1+s))-(a*phi:ℝ)*I=mark a (-(phi^2+s))
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Add the signed vertical steps a and a phi, then use 1+phi=phi^2; all four identities hold for every real a.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.scalar_roundtrip

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 13. Proof chapter: **P10**.

```lean
theorem scalar_roundtrip (h y : ℝ) : scalarDecode h (scalarEncode h y)=y
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Substitute e=floor(y/h) and r=y-h*e into h*e+r, for every real h including totalized division at zero.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.scalar_bounds

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 16. Proof chapter: **P10**.

```lean
theorem scalar_bounds (h y : ℝ) (hh : 0 < h) :
    0 ≤ (scalarEncode h y).2 ∧ (scalarEncode h y).2 < h
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiply the floor inequalities by h>0 and rearrange to 0<=r<h.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.scalar_canonical

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 25. Proof chapter: **P10**.

```lean
theorem scalar_canonical (h η : ℝ) (e : ℤ) (hh : 0 < h)
    (hη : 0 ≤ η ∧ η < h) : scalarEncode h (h*e+η)=(e,η)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For integer e and 0<=eta<h, prove e<=(he+eta)/h<e+1, then recover the residual by subtraction.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.rational_residual

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 34. Proof chapter: **P10**.

```lean
theorem rational_residual (d : ℕ) : q*d-(F d:ℝ)=(rho d:ℝ)/S
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Divide the natural Euclidean identity by S>0, for every natural d.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.real_residual

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 41. Proof chapter: **P10**.

```lean
theorem real_residual (d : ℕ) (hd : d < domainSize) :
    lam*d-(Int.floor (lam*d):ℝ)=(rho d:ℝ)/S+(lam-q)*d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: On D substitute the certified real floor successor F(d), then add and subtract q*d.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.positive_residual_difference

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 48. Proof chapter: **P10**.

```lean
theorem positive_residual_difference (d : ℕ) (hd : 0 < d) :
    0 < (lam-q)*(d:ℝ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Multiply lambda-q>0 by positive d; no finite-domain restriction is required for this inequality.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.grid_finite_interface

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 51. Proof chapter: **P10**.

```lean
theorem grid_finite_interface (h : ℝ) (hh : 0 < h) (d : ℕ) (hd : d < domainSize) :
    quantizedStep h (h*d)=h*(F d:ℝ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Combine the signed-integer grid-coordinate identity with finite-domain floor agreement.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.grid_trajectory

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 58. Proof chapter: **P10**.

```lean
theorem grid_trajectory (h : ℝ) (hh : 0 < h) (n d : ℕ) (hd : d < domainSize) :
    (quantizedStep h)^[n] (h*d)=h*(F^[n] d:ℝ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on every natural n; apply grid_finite_interface at the current state and use forward invariance.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.repeated_rounding_counterexample

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 68. Proof chapter: **P10**.

```lean
theorem repeated_rounding_counterexample :
    (realStep lam)^[2] 26=2 ∧ Int.floor (lam^2*26)=3
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Compute F(26)=8 and F(8)=2 exactly, while rational bounds give 3<26lambda^2<4.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.ledger_interface

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 81. Proof chapter: **P10**.

```lean
theorem ledger_interface (d : ℕ) :
    Ledger.step Q S d=(F d:ℤ) ∧ Ledger.remainder Q S d=(rho d:ℤ)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For natural d, signed Euclidean division and remainder by the positive canonical constants agree with their natural-number counterparts.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.external_factorization

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 85. Proof chapter: **P10**.

```lean
theorem external_factorization (d : ℕ) :
    scalarEncode S ((Q:ℝ)*d)=((F d:ℤ),(rho d:ℝ))
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply scalar_canonical with h=S, e=F(d), eta=rho(d) and the Euclidean identity. This is only the supplied external interface.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.predecessor_inequalities

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 97. Proof chapter: **P10**.

```lean
theorem predecessor_inequalities (A B d e : ℤ) (hB : 0 < B) :
    Ledger.step A B d=e ↔ B*e ≤ A*d ∧ A*d < B*(e+1)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For B>0 characterize floor(Ad/B)=e by Be<=Ad<B(e+1), for all signed integers A,d,e.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.point_reconstruction

Source: [reference/Lean/Omega/Interface.lean](reference/Lean/Omega/Interface.lean), line 109. Proof chapter: **P10**.

```lean
theorem point_reconstruction (h : ℝ) (α : V) (frame : ℝ →ₗ[ℝ] V)
    (n : ℕ) (d : ℤ) :
    pointFromState h α frame
      (Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2)=
      pointFromState h α frame d
```

Section context: `variable {V : Type*} [AddCommGroup V] [Module ℝ V]`

Proof step: Substitute integer ledger roundtrip into alpha+frame(h*d), retaining arbitrary real h, center and real linear frame; injectivity is unnecessary for this equality.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.Ledger.euclidean_identity

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 28. Proof chapter: **P09**.

```lean
theorem euclidean_identity (A B d : ℤ) :
    B*step A B d + remainder A B d = A*d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use total Euclidean division x=B*ediv(x,B)+emod(x,B) at x=Ad, including B=0 and negative B.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.remainder_bounds

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 31. Proof chapter: **P09**.

```lean
theorem remainder_bounds (A B d : ℤ) (hB : 0 < B) :
    0 ≤ remainder A B d ∧ remainder A B d < B
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: For B>0, Euclidean remainder is in [0,B), with no assumption on A or d.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.one_step_inverse

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 35. Proof chapter: **P09**.

```lean
theorem one_step_inverse (A B d : ℤ) (hA : A ≠ 0) :
    (B*step A B d+remainder A B d)/A=d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Replace B*step+remainder by Ad and divide by nonzero A; B is arbitrary.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.roundtrip

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 40. Proof chapter: **P09**.

```lean
theorem roundtrip (A B : ℤ) (hA : A ≠ 0) (n : ℕ) (d : ℤ) :
    recover A B (encode A B n d).1 (encode A B n d).2=d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on ledger length: recover the first successor from the tail, then use one_step_inverse. A!=0, but B may be negative or zero.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.encode_length

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 49. Proof chapter: **P09**.

```lean
theorem encode_length (A B : ℤ) (n : ℕ) (d : ℤ) :
    (encode A B n d).2.length=n
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on depth: encoding prepends exactly one remainder to the tail; A and B are unrestricted.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.generated_admissible

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 55. Proof chapter: **P09**.

```lean
theorem generated_admissible (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)
    (n : ℕ) (d : ℤ) :
    Admissible A B (encode A B n d).1 (encode A B n d).2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on the generated tail, use roundtrip to identify its recovered successor, apply remainder bounds, and observe Ad is divisible by A.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.canonical_division

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 67. Proof chapter: **P09**.

```lean
theorem canonical_division (A B d e r : ℤ) (hB : 0 < B)
    (hr : 0 ≤ r ∧ r < B) (he : A*d=B*e+r) :
    step A B d=e ∧ remainder A B d=r
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: From Ad=Be+r and 0<=r<B with B>0 derive e<=Ad/B<e+1, then obtain quotient e and remainder r. A may be zero.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.admissible_roundtrip

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 78. Proof chapter: **P09**.

```lean
theorem admissible_roundtrip (A B : ℤ) (hB : 0 < B) (t : ℤ)
    (rs : List ℤ) (hv : Admissible A B t rs) :
    encode A B rs.length (recover A B t rs)=(t,rs)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on a proposed record. Reverse-step divisibility gives A*d=B*e+r even for A=0 under the total convention; canonical_division recovers its first transition and the induction hypothesis its tail. Only B>0 is required.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.encoding_injective

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 92. Proof chapter: **P09**.

```lean
theorem encoding_injective (A B : ℤ) (hA : A ≠ 0) (n : ℕ) :
    Function.Injective (encode A B n)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply recover to equal encodings and use roundtrip, for nonzero A and arbitrary B.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.admissibility_iff

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 98. Proof chapter: **P09**.

```lean
theorem admissibility_iff (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)
    (t : ℤ) (rs : List ℤ) :
    Admissible A B t rs ↔ ∃! d, encode A B rs.length d=(t,rs)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Generated records are admissible; admissible recovery re-encodes the exact record; encoding injectivity gives unique initial integer. Requires A!=0,B>0.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.weighted_identity

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 118. Proof chapter: **P09**.

```lean
theorem weighted_identity (A B : ℤ) (t : ℤ) (rs : List ℤ)
    (hv : Admissible A B t rs) :
    A^rs.length*recover A B t rs=B^rs.length*t+value A B rs
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Induct on the ordered list and multiply A*d=B*e+r by A^tail_length, substituting the tail polynomial identity. Only admissibility is assumed.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.encoded_weighted_identity

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 136. Proof chapter: **P09**.

```lean
theorem encoded_weighted_identity (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)
    (n : ℕ) (d : ℤ) :
    A^n*d=B^n*(encode A B n d).1+value A B (encode A B n d).2
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Apply weighted_identity to a generated admissible record and use encode_length and roundtrip; A!=0,B>0.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.Ledger.trajectory_reconstruction

Source: [reference/Lean/Omega/Ledger.lean](reference/Lean/Omega/Ledger.lean), line 143. Proof chapter: **P09**.

```lean
theorem trajectory_reconstruction (A B : ℤ) (hA : A ≠ 0) (n j : ℕ) (d : ℤ) :
    (step A B)^[j]
      (recover A B (encode A B n d).1 (encode A B n d).2)=(step A B)^[j] d
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Replace the recovered seed by d using roundtrip before applying any natural number j of further steps, even beyond retained depth.

Evidence: Analytic induction or implication for the universal theorem; exact finite regression checks separately exercise the implementation.

## Omega.central_provenance_theorem

Source: [reference/Lean/Omega/Main.lean](reference/Lean/Omega/Main.lean), line 13. Proof chapter: **P13**.

```lean
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))
```

Section 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.

## Omega.mark_dot

Source: [reference/Lean/Omega/Metrics.lean](reference/Lean/Omega/Metrics.lean), line 9. Proof chapter: **P05**.

```lean
theorem mark_dot (a z w : ℝ) :
    ⟪mark a z,mark a w⟫=a^2*(c^2+z*w)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Expand the real Euclidean dot product coordinate by coordinate for all real a,z,w.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_radius

Source: [reference/Lean/Omega/Metrics.lean](reference/Lean/Omega/Metrics.lean), line 15. Proof chapter: **P05**.

```lean
theorem mark_radius (a z : ℝ) (ha : 0 < a) :
    ‖mark a z‖=a*Real.sqrt (c^2+z^2)
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The squared norm is a^2(c^2+z^2); take nonnegative square roots and use a>0.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_angle_cosine

Source: [reference/Lean/Omega/Metrics.lean](reference/Lean/Omega/Metrics.lean), line 22. Proof chapter: **P05**.

```lean
theorem mark_angle_cosine (a z w : ℝ) (ha : 0 < a) :
    Real.cos (angle (mark a z) (mark a w))=
      (c^2+z*w)/(Real.sqrt (c^2+z^2)*Real.sqrt (c^2+w^2))
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Use the dot-over-product-of-norms formula; c>0 and a>0 make both radii nonzero, so cancellation is legitimate.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.seed_angle

Source: [reference/Lean/Omega/Metrics.lean](reference/Lean/Omega/Metrics.lean), line 32. Proof chapter: **P05**.

```lean
theorem seed_angle (a : ℝ) (ha : 0 < a) :
    angle (mark a s) (mark a (-s))=epsilon
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: The seed cosine is c^2-s^2=cos(2delta)=cos(epsilon). Both angles lie in [0,pi], where cosine is injective.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.triangle_area

Source: [reference/Lean/Omega/Metrics.lean](reference/Lean/Omega/Metrics.lean), line 51. Proof chapter: **P05**.

```lean
theorem triangle_area (a z w : ℝ) :
    triangleArea a z w=a^2*c/2*|z-w|
```

Section context: `No section-level variable declarations before this theorem; see the exact declaration and module definitions.`

Proof step: Take half the absolute determinant a^2 c(w-z); a^2>=0 and c>0 give the formula for every real a.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.placed_distance

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 17. Proof chapter: **P03**.

```lean
theorem placed_distance (α : V) (E : ℂ →ₗᵢ[ℝ] V) (z w : ℂ) :
    dist (place α E z) (place α E w)=dist z w
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Translation cancels in differences and E preserves norms.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.placed_arc_derivative

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 21. Proof chapter: **P03**.

```lean
theorem placed_arc_derivative (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a t : ℝ) :
    HasDerivAt (placedArc α E a) (E (circleMap 0 a t*I)) t
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: A linear isometry is continuous; apply its derivative to gamma'_a(t)=gamma_a(t)i and add a constant center. This derivative statement holds for every real a.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.placed_G

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 32. Proof chapter: **P03**.

```lean
theorem placed_G (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : placedG α E a=G a
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Apply distance preservation separately to both outer segments; valid for every real a.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.placed_C

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 35. Proof chapter: **P03**.

```lean
theorem placed_C (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a : ℝ) : placedC α E a=C a
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: At every t, the placed derivative is E(gamma'_a(t)); its norm equals the unplaced derivative norm. Integrate equal functions, for every real a.

Evidence: Analytic real/calculus proof text with stated standard mathematical foundations; Julia is not a kernel checker for this inference.

## Omega.provenance_all_placements

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 42. Proof chapter: **P03**.

```lean
theorem provenance_all_placements (α : V) (E : ℂ →ₗᵢ[ℝ] V)
    (a : ℝ) (ha : 0 < a) :
    placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧
    placedG α E a/(placedG α E a+placedC α E a)=lam
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Substitute placed_G, placed_C and the positive-radius geometric provenance identities.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.mark_scale

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 51. Proof chapter: **P03**.

```lean
theorem mark_scale (k a z : ℝ) : (k:ℝ) • mark a z=mark (k*a) z
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Multiply both coordinates by real k; obtain the mark with radius ka, with no sign restriction.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.circle_scale

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 55. Proof chapter: **P03**.

```lean
theorem circle_scale (k a t : ℝ) : (k:ℝ) • circleMap 0 a t=circleMap 0 (k*a) t
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Multiply the cosine and sine coordinates by k, for all real k,a,t.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.outline_scale

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 58. Proof chapter: **P03**.

```lean
theorem outline_scale (k a : ℝ) : ((k:ℝ) • ·) '' outline a=outline (k*a)
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Apply mark_scale and circle_scale pointwise to the three parameter images and use image of union; zero and negative scales are included.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.placed_homothety

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 62. Proof chapter: **P03**.

```lean
theorem placed_homothety (α : V) (E : ℂ →ₗᵢ[ℝ] V) (k a : ℝ) :
    homothety k α '' placedOutline α E a=placedOutline α E (k*a)
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Cancel alpha in the centered homothety and move real scaling through E, then apply outline_scale.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.readout_scale

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 69. Proof chapter: **P03**.

```lean
theorem readout_scale (k a : ℝ) (hk : 0 < k) (ha : 0 < a) :
    G (k*a)=k*G a ∧ C (k*a)=k*C a
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: For k>0 and a>0 use G(ka)=ka phi and C(ka)=ka pi and factor k.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.

## Omega.curve_reconstruction

Source: [reference/Lean/Omega/Placement.lean](reference/Lean/Omega/Placement.lean), line 76. Proof chapter: **P03**.

```lean
theorem curve_reconstruction (α : V) (E : ℂ →ₗᵢ[ℝ] V)
    (h : ℝ) (n : ℕ) (d : ℤ) :
    placedOutline α E
      (h*Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2)=
    placedOutline α E (h*d)
```

Section context: `variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]`

Proof step: Substitute integer ledger roundtrip into radius h*d; retain h,alpha,E. The set equality holds for every real h and signed integer d.

Evidence: Analytic argument; exact polynomial certificates and/or rational inequalities verify the applicable algebraic steps.