# Every supplied named Lean theorem, indexed once. Source declarations are verbatim.
format_version = 1
theorem_count = 147

[[theorem]]
name = "Omega.weighted_mean"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 11
chapter = "P06"
statement = "theorem weighted_mean (a x : ℝ) (ha : 0 < a) :\n    (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."

[[theorem]]
name = "Omega.displacement_conjugacy"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 20
chapter = "P06"
statement = "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."

[[theorem]]
name = "Omega.affine_iterate"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 24
chapter = "P06"
statement = "theorem affine_iterate (n : ℕ) (x : ℝ) :\n    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."

[[theorem]]
name = "Omega.homothety_comp"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 39
chapter = "P06"
statement = "theorem homothety_comp (k l : ℝ) (α z : V) :\n    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."

[[theorem]]
name = "Omega.homothety_one"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 43
chapter = "P06"
statement = "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."

[[theorem]]
name = "Omega.observation_commutes"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 46
chapter = "P06"
statement = "theorem observation_commutes (L : V →ₗ[ℝ] ℝ) (k : ℝ) (α z : V) :\n    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."

[[theorem]]
name = "Omega.observation_iterate"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 50
chapter = "P06"
statement = "theorem observation_iterate (L : V →ₗ[ℝ] ℝ) (n : ℕ) (α z : V) :\n    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."

[[theorem]]
name = "Omega.real_time_semigroup"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 55
chapter = "P06"
statement = "theorem real_time_semigroup (t u : ℝ) (α z : V) :\n    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."

[[theorem]]
name = "Omega.arbitrary_intercept_defect"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 59
chapter = "P06"
statement = "theorem arbitrary_intercept_defect (L : V →ₗ[ℝ] ℝ) (k b : ℝ) (α z : V) :\n    (b + L (homothety k α z - α)) - Tk k (b + L (z - α)) =\n      (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."

[[theorem]]
name = "Omega.grid_interface"
module = "Affine"
source = "reference/Lean/Omega/Affine.lean"
line = 68
chapter = "P06"
statement = "theorem grid_interface (h : ℝ) (hh : 0 < h) (d : ℤ) :\n    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."

[[theorem]]
name = "Omega.phi_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 24
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.phi_sq"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 26
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.phi_bounds"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 31
chapter = "P01"
statement = "theorem phi_bounds : 1.61803398874989484820 < phi ∧\n    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}."

[[theorem]]
name = "Omega.denominator_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 37
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.lam_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 39
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.lam_lt_one"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 41
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.shares_sum"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 46
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.mu_eq_one_sub"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 50
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.lam_bounds"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 52
chapter = "P01"
statement = "theorem lam_bounds : (339949771344778 : ℝ) / 10^15 < lam ∧\n    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}."

[[theorem]]
name = "Omega.q_lt_lam"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 66
chapter = "P01"
statement = "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}."

[[theorem]]
name = "Omega.lam_lt_q_plus"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 71
chapter = "P01"
statement = "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}."

[[theorem]]
name = "Omega.delta_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 76
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.delta_lt_half_pi"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 78
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.s_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 82
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.c_pos"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 86
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.sc_identity"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 92
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.one_arcsecond"
module = "Constants"
source = "reference/Lean/Omega/Constants.lean"
line = 94
chapter = "P01"
statement = "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."

[[theorem]]
name = "Omega.seeds_distinct"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 8
chapter = "P04"
statement = "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."

[[theorem]]
name = "Omega.marks_collinear"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 14
chapter = "P04"
statement = "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."

[[theorem]]
name = "Omega.marks_affine_dimension"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 21
chapter = "P04"
statement = "theorem marks_affine_dimension (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.seed_linear_combination"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 29
chapter = "P04"
statement = "theorem seed_linear_combination (a : ℝ) (ha : 0 < a) (z : ℂ) :\n    ((z.re/(a*c)+z.im/(a*s))/2) • mark a s+\n    ((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."

[[theorem]]
name = "Omega.centered_span"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 41
chapter = "P04"
statement = "theorem centered_span (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.center_relative_rank"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 52
chapter = "P04"
statement = "theorem center_relative_rank (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.center_adjoined_affine_dimension"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 56
chapter = "P04"
statement = "theorem center_adjoined_affine_dimension (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.moment_matrix"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 73
chapter = "P04"
statement = "theorem moment_matrix (a : ℝ) :\n    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."

[[theorem]]
name = "Omega.coordinates_rank"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 79
chapter = "P04"
statement = "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."

[[theorem]]
name = "Omega.gram_rank"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 102
chapter = "P04"
statement = "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."

[[theorem]]
name = "Omega.gram_entries"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 105
chapter = "P04"
statement = "theorem gram_entries (a : ℝ) (i j : Fin 6) :\n    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."

[[theorem]]
name = "Omega.embedded_center_relative_rank"
module = "Dimension"
source = "reference/Lean/Omega/Dimension.lean"
line = 112
chapter = "P04"
statement = "theorem embedded_center_relative_rank {V : Type*} [AddCommGroup V] [Module ℝ V]\n    (E : ℂ →ₗ[ℝ] V) (hE : Function.Injective E) (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.step_threshold"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 9
chapter = "P12"
statement = "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."

[[theorem]]
name = "Omega.extinction_threshold"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 13
chapter = "P12"
statement = "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."

[[theorem]]
name = "Omega.threshold_values"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 20
chapter = "P12"
statement = "theorem threshold_values : (List.range 11).map threshold=\n    [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."

[[theorem]]
name = "Omega.extinction_by_ten"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 23
chapter = "P12"
statement = "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."

[[theorem]]
name = "Omega.deepest_seeds"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 30
chapter = "P12"
statement = "theorem deepest_seeds (d : ℕ) (hd : d < domainSize) :\n    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."

[[theorem]]
name = "Omega.all_twenty_three_steps"
module = "Extinction"
source = "reference/Lean/Omega/Extinction.lean"
line = 39
chapter = "P12"
statement = "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."

[[theorem]]
name = "Omega.gcd_constants"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 9
chapter = "P11"
statement = "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."

[[theorem]]
name = "Omega.inverse_identity"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 10
chapter = "P11"
statement = "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."

[[theorem]]
name = "Omega.remainder_halved"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 12
chapter = "P11"
statement = "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."

[[theorem]]
name = "Omega.first_remainder_reconstruction"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 20
chapter = "P11"
statement = "theorem first_remainder_reconstruction (d : ℕ) (hd : d < period) :\n    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."

[[theorem]]
name = "Omega.first_remainder_injective"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 32
chapter = "P11"
statement = "theorem first_remainder_injective :\n    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."

[[theorem]]
name = "Omega.first_remainder_injective_domain"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 39
chapter = "P11"
statement = "theorem first_remainder_injective_domain :\n    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."

[[theorem]]
name = "Omega.finite_gap_certificate"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 50
chapter = "P11"
statement = "theorem finite_gap_certificate :\n    (List.range 128).all (fun b => (List.range 256).all\n      (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."

[[theorem]]
name = "Omega.certified_gap"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 54
chapter = "P11"
statement = "theorem certified_gap (d : ℕ) (hd : d < domainSize) :\n    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."

[[theorem]]
name = "Omega.minimum_gap_attained"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 65
chapter = "P11"
statement = "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."

[[theorem]]
name = "Omega.finite_certificate_inequality"
module = "Finite"
source = "reference/Lean/Omega/Finite.lean"
line = 67
chapter = "P11"
statement = "theorem finite_certificate_inequality :\n    (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."

[[theorem]]
name = "Omega.S_pos"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 10
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.Q_pos"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 11
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.Q_lt_S"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 12
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.division_identity"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 14
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.remainder_bound"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 17
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.step_zero"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 19
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.step_lt"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 21
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.step_le"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 25
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.forward_invariant"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 30
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.step_monotone"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 33
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.q_in_interval"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 42
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.lam_in_interval"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 43
chapter = "P07"
statement = "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}."

[[theorem]]
name = "Omega.floor_q"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 48
chapter = "P07"
statement = "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."

[[theorem]]
name = "Omega.no_interior_boundary"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 65
chapter = "P07"
statement = "theorem no_interior_boundary (d : ℕ) (hd : d < domainSize) (k : ℤ)\n    (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."

[[theorem]]
name = "Omega.floor_agreement_of_interval"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 81
chapter = "P07"
statement = "theorem floor_agreement_of_interval (r : ℝ) (hr : lower ≤ r ∧ r < upper)\n    (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."

[[theorem]]
name = "Omega.exact_parameter_interval"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 107
chapter = "P07"
statement = "theorem exact_parameter_interval (r : ℝ) :\n    (∀ d : ℕ, d < domainSize → Int.floor (r*d) = (F d:ℤ)) ↔\n      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."

[[theorem]]
name = "Omega.certified_floor_equality"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 120
chapter = "P07"
statement = "theorem certified_floor_equality (d : ℕ) (hd : d < domainSize) :\n    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."

[[theorem]]
name = "Omega.trajectory_equality"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 126
chapter = "P07"
statement = "theorem trajectory_equality (r : ℝ) (hr : lower ≤ r ∧ r < upper)\n    (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."

[[theorem]]
name = "Omega.truncation_le"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 139
chapter = "P08"
statement = "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."

[[theorem]]
name = "Omega.truncation_succ"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 144
chapter = "P08"
statement = "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."

[[theorem]]
name = "Omega.truncation_monotone"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 159
chapter = "P08"
statement = "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."

[[theorem]]
name = "Omega.truncation_seven"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 161
chapter = "P08"
statement = "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."

[[theorem]]
name = "Omega.truncation_eight"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 169
chapter = "P08"
statement = "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."

[[theorem]]
name = "Omega.precision_threshold"
module = "Floor"
source = "reference/Lean/Omega/Floor.lean"
line = 178
chapter = "P08"
statement = "theorem precision_threshold (p : ℕ) :\n    (∀ 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."

[[theorem]]
name = "Omega.arc_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 24
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.semicircle_retained"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 28
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.semicircle_in_outline"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 34
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.major_arc_no_retracing"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 38
chapter = "P02"
statement = "theorem major_arc_no_retracing (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.upper_seed_endpoint"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 45
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.lower_seed_endpoint"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 48
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.mark_re"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 53
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.mark_im"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 54
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.bilateral_reflection"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 56
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.mark_distance"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 59
chapter = "P02"
statement = "theorem mark_distance (a z w : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.inner_extension_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 68
chapter = "P02"
statement = "theorem inner_extension_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.outer_extension_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 74
chapter = "P02"
statement = "theorem outer_extension_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.negative_outer_extension_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 80
chapter = "P02"
statement = "theorem negative_outer_extension_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.total_extension_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 86
chapter = "P02"
statement = "theorem total_extension_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.chord_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 91
chapter = "P02"
statement = "theorem chord_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.outer_segment_retained"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 96
chapter = "P02"
statement = "theorem outer_segment_retained (a : ℝ) :\n    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."

[[theorem]]
name = "Omega.G_eq"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 110
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.C_eq"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 113
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.W_eq"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 117
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.geometric_provenance"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 121
chapter = "P02"
statement = "theorem geometric_provenance (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.outline_length"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 130
chapter = "P02"
statement = "theorem outline_length (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.reference_not_outline"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 139
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.marked_coordinate_uniqueness"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 146
chapter = "P02"
statement = "theorem marked_coordinate_uniqueness (a : ℝ) (p : Fin 6 → ℂ)\n    (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."

[[theorem]]
name = "Omega.heights_strictly_ordered"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 153
chapter = "P02"
statement = "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."

[[theorem]]
name = "Omega.sequential_extensions"
module = "Geometry"
source = "reference/Lean/Omega/Geometry.lean"
line = 158
chapter = "P02"
statement = "theorem sequential_extensions (a : ℝ) :\n    mark a s+(a:ℂ)*I=mark a (1+s) ∧\n    mark a (1+s)+(a*phi:ℝ)*I=mark a (phi^2+s) ∧\n    mark a (-s)-(a:ℂ)*I=mark a (-(1+s)) ∧\n    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."

[[theorem]]
name = "Omega.scalar_roundtrip"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 13
chapter = "P10"
statement = "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."

[[theorem]]
name = "Omega.scalar_bounds"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 16
chapter = "P10"
statement = "theorem scalar_bounds (h y : ℝ) (hh : 0 < h) :\n    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."

[[theorem]]
name = "Omega.scalar_canonical"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 25
chapter = "P10"
statement = "theorem scalar_canonical (h η : ℝ) (e : ℤ) (hh : 0 < h)\n    (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."

[[theorem]]
name = "Omega.rational_residual"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 34
chapter = "P10"
statement = "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."

[[theorem]]
name = "Omega.real_residual"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 41
chapter = "P10"
statement = "theorem real_residual (d : ℕ) (hd : d < domainSize) :\n    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."

[[theorem]]
name = "Omega.positive_residual_difference"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 48
chapter = "P10"
statement = "theorem positive_residual_difference (d : ℕ) (hd : 0 < d) :\n    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."

[[theorem]]
name = "Omega.grid_finite_interface"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 51
chapter = "P10"
statement = "theorem grid_finite_interface (h : ℝ) (hh : 0 < h) (d : ℕ) (hd : d < domainSize) :\n    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."

[[theorem]]
name = "Omega.grid_trajectory"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 58
chapter = "P10"
statement = "theorem grid_trajectory (h : ℝ) (hh : 0 < h) (n d : ℕ) (hd : d < domainSize) :\n    (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."

[[theorem]]
name = "Omega.repeated_rounding_counterexample"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 68
chapter = "P10"
statement = "theorem repeated_rounding_counterexample :\n    (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."

[[theorem]]
name = "Omega.ledger_interface"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 81
chapter = "P10"
statement = "theorem ledger_interface (d : ℕ) :\n    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."

[[theorem]]
name = "Omega.external_factorization"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 85
chapter = "P10"
statement = "theorem external_factorization (d : ℕ) :\n    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."

[[theorem]]
name = "Omega.predecessor_inequalities"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 97
chapter = "P10"
statement = "theorem predecessor_inequalities (A B d e : ℤ) (hB : 0 < B) :\n    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."

[[theorem]]
name = "Omega.point_reconstruction"
module = "Interface"
source = "reference/Lean/Omega/Interface.lean"
line = 109
chapter = "P10"
statement = "theorem point_reconstruction (h : ℝ) (α : V) (frame : ℝ →ₗ[ℝ] V)\n    (n : ℕ) (d : ℤ) :\n    pointFromState h α frame\n      (Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2)=\n      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."

[[theorem]]
name = "Omega.Ledger.euclidean_identity"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 28
chapter = "P09"
statement = "theorem euclidean_identity (A B d : ℤ) :\n    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."

[[theorem]]
name = "Omega.Ledger.remainder_bounds"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 31
chapter = "P09"
statement = "theorem remainder_bounds (A B d : ℤ) (hB : 0 < B) :\n    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."

[[theorem]]
name = "Omega.Ledger.one_step_inverse"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 35
chapter = "P09"
statement = "theorem one_step_inverse (A B d : ℤ) (hA : A ≠ 0) :\n    (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."

[[theorem]]
name = "Omega.Ledger.roundtrip"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 40
chapter = "P09"
statement = "theorem roundtrip (A B : ℤ) (hA : A ≠ 0) (n : ℕ) (d : ℤ) :\n    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."

[[theorem]]
name = "Omega.Ledger.encode_length"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 49
chapter = "P09"
statement = "theorem encode_length (A B : ℤ) (n : ℕ) (d : ℤ) :\n    (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."

[[theorem]]
name = "Omega.Ledger.generated_admissible"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 55
chapter = "P09"
statement = "theorem generated_admissible (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)\n    (n : ℕ) (d : ℤ) :\n    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."

[[theorem]]
name = "Omega.Ledger.canonical_division"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 67
chapter = "P09"
statement = "theorem canonical_division (A B d e r : ℤ) (hB : 0 < B)\n    (hr : 0 ≤ r ∧ r < B) (he : A*d=B*e+r) :\n    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."

[[theorem]]
name = "Omega.Ledger.admissible_roundtrip"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 78
chapter = "P09"
statement = "theorem admissible_roundtrip (A B : ℤ) (hB : 0 < B) (t : ℤ)\n    (rs : List ℤ) (hv : Admissible A B t rs) :\n    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."

[[theorem]]
name = "Omega.Ledger.encoding_injective"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 92
chapter = "P09"
statement = "theorem encoding_injective (A B : ℤ) (hA : A ≠ 0) (n : ℕ) :\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."

[[theorem]]
name = "Omega.Ledger.admissibility_iff"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 98
chapter = "P09"
statement = "theorem admissibility_iff (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)\n    (t : ℤ) (rs : List ℤ) :\n    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."

[[theorem]]
name = "Omega.Ledger.weighted_identity"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 118
chapter = "P09"
statement = "theorem weighted_identity (A B : ℤ) (t : ℤ) (rs : List ℤ)\n    (hv : Admissible A B t rs) :\n    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."

[[theorem]]
name = "Omega.Ledger.encoded_weighted_identity"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 136
chapter = "P09"
statement = "theorem encoded_weighted_identity (A B : ℤ) (hA : A ≠ 0) (hB : 0 < B)\n    (n : ℕ) (d : ℤ) :\n    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."

[[theorem]]
name = "Omega.Ledger.trajectory_reconstruction"
module = "Ledger"
source = "reference/Lean/Omega/Ledger.lean"
line = 143
chapter = "P09"
statement = "theorem trajectory_reconstruction (A B : ℤ) (hA : A ≠ 0) (n j : ℕ) (d : ℤ) :\n    (step A B)^[j]\n      (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."

[[theorem]]
name = "Omega.central_provenance_theorem"
module = "Main"
source = "reference/Lean/Omega/Main.lean"
line = 13
chapter = "P13"
statement = "theorem central_provenance_theorem\n    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]\n    (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a h : ℝ) (ha : 0 < a) (hh : 0 < h) :\n    (placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧\n      placedG α E a/(placedG α E a+placedC α E a)=lam) ∧\n    (∀ x : ℝ, (G a*x+C a)/(G a+C a)=T x) ∧\n    (∀ d : ℕ, d < domainSize → Int.floor (lam*d)=(F d:ℤ)) ∧\n    (∀ n d : ℕ, d < domainSize →\n      (quantizedStep h)^[n] (h*d)=h*(F^[n] d:ℝ)) ∧\n    (∀ n : ℕ, ∀ d : ℤ,\n      Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2=d) ∧\n    (∀ t : ℤ, ∀ rs : List ℤ, Ledger.Admissible Q S t rs ↔\n      ∃! 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."

[[theorem]]
name = "Omega.mark_dot"
module = "Metrics"
source = "reference/Lean/Omega/Metrics.lean"
line = 9
chapter = "P05"
statement = "theorem mark_dot (a z w : ℝ) :\n    ⟪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."

[[theorem]]
name = "Omega.mark_radius"
module = "Metrics"
source = "reference/Lean/Omega/Metrics.lean"
line = 15
chapter = "P05"
statement = "theorem mark_radius (a z : ℝ) (ha : 0 < a) :\n    ‖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."

[[theorem]]
name = "Omega.mark_angle_cosine"
module = "Metrics"
source = "reference/Lean/Omega/Metrics.lean"
line = 22
chapter = "P05"
statement = "theorem mark_angle_cosine (a z w : ℝ) (ha : 0 < a) :\n    Real.cos (angle (mark a z) (mark a w))=\n      (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."

[[theorem]]
name = "Omega.seed_angle"
module = "Metrics"
source = "reference/Lean/Omega/Metrics.lean"
line = 32
chapter = "P05"
statement = "theorem seed_angle (a : ℝ) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.triangle_area"
module = "Metrics"
source = "reference/Lean/Omega/Metrics.lean"
line = 51
chapter = "P05"
statement = "theorem triangle_area (a z w : ℝ) :\n    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."

[[theorem]]
name = "Omega.placed_distance"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 17
chapter = "P03"
statement = "theorem placed_distance (α : V) (E : ℂ →ₗᵢ[ℝ] V) (z w : ℂ) :\n    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."

[[theorem]]
name = "Omega.placed_arc_derivative"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 21
chapter = "P03"
statement = "theorem placed_arc_derivative (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a t : ℝ) :\n    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."

[[theorem]]
name = "Omega.placed_G"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 32
chapter = "P03"
statement = "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."

[[theorem]]
name = "Omega.placed_C"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 35
chapter = "P03"
statement = "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."

[[theorem]]
name = "Omega.provenance_all_placements"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 42
chapter = "P03"
statement = "theorem provenance_all_placements (α : V) (E : ℂ →ₗᵢ[ℝ] V)\n    (a : ℝ) (ha : 0 < a) :\n    placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧\n    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."

[[theorem]]
name = "Omega.mark_scale"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 51
chapter = "P03"
statement = "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."

[[theorem]]
name = "Omega.circle_scale"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 55
chapter = "P03"
statement = "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."

[[theorem]]
name = "Omega.outline_scale"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 58
chapter = "P03"
statement = "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."

[[theorem]]
name = "Omega.placed_homothety"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 62
chapter = "P03"
statement = "theorem placed_homothety (α : V) (E : ℂ →ₗᵢ[ℝ] V) (k a : ℝ) :\n    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."

[[theorem]]
name = "Omega.readout_scale"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 69
chapter = "P03"
statement = "theorem readout_scale (k a : ℝ) (hk : 0 < k) (ha : 0 < a) :\n    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."

[[theorem]]
name = "Omega.curve_reconstruction"
module = "Placement"
source = "reference/Lean/Omega/Placement.lean"
line = 76
chapter = "P03"
statement = "theorem curve_reconstruction (α : V) (E : ℂ →ₗᵢ[ℝ] V)\n    (h : ℝ) (n : ℕ) (d : ℤ) :\n    placedOutline α E\n      (h*Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2)=\n    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."