IndisputableMonolith.Foundation.DeltaSpine.LadderRatioBounds

   1import IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
   2import IndisputableMonolith.Foundation.DeltaSpine.CostUniqueness
   3
   4/-!
   5# LadderRatioBounds: forced φ-ladder ratios with certified rational brackets (sigma0)
   6
   7**One dimensionless forced ratio, carried end-to-end at sigma0, with rational
   8bounds that both the kernel (`decide`) and the runtime (`#eval`) certify.**
   9
  10The RS mass law places every rung of the spectrum on the φ-ladder: two states
  11separated by an integer rung gap `k` (with the same yardstick and gap class)
  12stand in the exact dimensionless ratio `φ^k`. `φ` itself (T6) is the primitive
  13forced dimensionless ratio; every ladder gap is one of its integer powers.
  14
  15This module makes that ratio *computable and certified without the continuum*:
  16
  171. `phiPow k = φ^k` as an explicit element of ℤ[φ] (structural recursion, so it
  18   reduces under both the kernel and the compiler — `#eval (phiPow 5)` prints
  19   `⟨3, 5⟩`, i.e. `3 + 5φ`, and `decide` reduces it the same way).
  202. `RatLt p q x` / `RatGt p q x`: the decidable integer predicates "`p/q < x`"
  21   and "`x < p/q`" on ℤ[φ], defined by reusing the sigma0 sign predicate `IsPos`
  22   on the witness `q·x − p`. Because `IsPos` is decidable and choice-free, every
  23   concrete bracket closes by `decide` inside `{propext, Quot.sound}` and is
  24   independently confirmed by `#eval`.
  253. Certified brackets for φ and the representative rungs φ⁵, φ⁸ (the octave),
  26   tight to the stated rational precision — e.g. `1618033/1000000 < φ < 1618034/1000000`.
  27
  28The mechanism is exactly the √5-irrationality machinery already proved at sigma0
  29in `DeltaSpine.GoldenInt`: `p/q < a + bφ` reduces to a sign question about
  30`s + t√5` with `s, t ∈ ℤ`, decided by comparing `s²` with `5t²` (a tie is
  31impossible because √5 is irrational, `int_sq_eq_five_sq`). No `Real.sqrt`, no
  32`Float`, no `native_decide` (which would inject `ofReduceBool`, breaking sigma0).
  33
  34The bridge showing these brackets are genuine bounds on the *real* ratio
  35`φ^k ∈ ℝ` is `DeltaSpine.GoldenIntReal` (sigma1 CHOICE): the ordering and the
  36arithmetic are forced at sigma0; only the evaluation into ℝ costs
  37`Classical.choice`.
  38
  39**Verdict target: sigma0 DELTA_FORCED** — every theorem here closes within
  40`{propext, Quot.sound}`. Audit with `scripts/sigma_audit.py`.
  41
  42Delta Forcing Spectrum program: `Delta_Forcing_Spectrum_20260626.tex`.
  43-/
  44
  45namespace IndisputableMonolith
  46namespace Foundation
  47namespace DeltaSpine
  48namespace GoldenInt
  49
  50/-! ## The computable φ-power ladder -/
  51
  52/-- `φ^n` as an explicit element of ℤ[φ], by structural recursion. Unlike
  53    `phiZpow` (which routes through the unit group and does not reduce under
  54    `decide`/`#eval`), this reduces cleanly in the kernel and the compiler:
  55    `phiPow n = ⟨F(n−1), F(n)⟩` where `F` is Fibonacci. -/
  56def phiPow : ℕ → GoldenInt
  57  | 0 => 1
  58  | (n + 1) => phiPow n * phi
  59
  60@[simp] theorem phiPow_zero : phiPow 0 = 1 := rfl
  61
  62@[simp] theorem phiPow_succ (n : ℕ) : phiPow (n + 1) = phiPow n * phi := rfl
  63
  64theorem phiPow_one : phiPow 1 = phi := by decide
  65
  66/-- `φ⁵ = 5φ + 3 = ⟨3, 5⟩` — kernel computation. -/
  67theorem phiPow_five : phiPow 5 = ⟨3, 5⟩ := by decide
  68
  69/-- `φ⁸ = 21φ + 13 = ⟨13, 21⟩` (the octave rung) — kernel computation. -/
  70theorem phiPow_eight : phiPow 8 = ⟨13, 21⟩ := by decide
  71
  72/-- The computable ladder agrees with the unit-group ladder of
  73    `DeltaSpine.CostUniqueness` on ℕ, so these brackets are statements about
  74    the same `φⁿ` that carries `traceZ`/`Jdouble` (the T5 node). -/
  75theorem phiPow_eq_phiZpow (n : ℕ) : phiPow n = phiZpow (n : ℤ) := by
  76  induction n with
  77  | zero =>
  78      have e : ((0 : ℕ) : ℤ) = 0 := by decide
  79      rw [phiPow_zero, e, phiZpow_zero]
  80  | succ k ih =>
  81      have e : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by omega
  82      rw [phiPow_succ, ih, e, phiZpow_add, phiZpow_one]
  83
  84/-! ## Decidable rational brackets on ℤ[φ]
  85
  86`p/q < a + bφ` (for `q > 0`) iff `0 < q·(a+bφ) − p`, i.e. `IsPos ⟨q·a − p, q·b⟩`.
  87Reusing the sigma0 sign predicate keeps everything decidable and choice-free. -/
  88
  89/-- The witness element `q·x − p ∈ ℤ[φ]` whose sign decides `p/q ⋚ x`. -/
  90def ratWitness (p q : ℤ) (x : GoldenInt) : GoldenInt := ⟨q * x.a - p, q * x.b⟩
  91
  92/-- The rational `p/q` lies strictly below `x` (interpreted over the reals when
  93    `q > 0`). Decidable integer predicate: `0 < q·x − p`. -/
  94def RatLt (p q : ℤ) (x : GoldenInt) : Prop := IsPos (ratWitness p q x)
  95
  96/-- The rational `p/q` lies strictly above `x` (interpreted over the reals when
  97    `q > 0`). Decidable integer predicate: `0 < p − q·x`. -/
  98def RatGt (p q : ℤ) (x : GoldenInt) : Prop := IsPos (ratWitness (-p) q (-x))
  99
 100instance (p q : ℤ) (x : GoldenInt) : Decidable (RatLt p q x) := by
 101  unfold RatLt; infer_instance
 102
 103instance (p q : ℤ) (x : GoldenInt) : Decidable (RatGt p q x) := by
 104  unfold RatGt; infer_instance
 105
 106/-! ## Certified brackets
 107
 108Each bracket is a sigma0 theorem (closed by kernel `decide`, hence in
 109`{propext, Quot.sound}`) and is independently confirmed by `#eval` (runtime). -/
 110
 111/-- **φ, lower bracket**: `1.618033 < φ`. -/
 112theorem phi_lower : RatLt 1618033 1000000 phi := by decide
 113
 114/-- **φ, upper bracket**: `φ < 1.618034`. -/
 115theorem phi_upper : RatGt 1618034 1000000 phi := by decide
 116
 117/-- **φ⁵, lower bracket**: `11.09 < φ⁵` (`φ⁵ ≈ 11.0902`). -/
 118theorem phi5_lower : RatLt 1109 100 (phiPow 5) := by decide
 119
 120/-- **φ⁵, upper bracket**: `φ⁵ < 11.10`. -/
 121theorem phi5_upper : RatGt 1110 100 (phiPow 5) := by decide
 122
 123/-- **φ⁸, lower bracket**: `46.978 < φ⁸` (`φ⁸ ≈ 46.9787`, the octave rung). -/
 124theorem phi8_lower : RatLt 46978 1000 (phiPow 8) := by decide
 125
 126/-- **φ⁸, upper bracket**: `φ⁸ < 46.979`. -/
 127theorem phi8_upper : RatGt 46979 1000 (phiPow 8) := by decide
 128
 129/-- **Forced-ratio thread, delta-forced (sigma0)**: the primitive forced
 130    dimensionless ratio φ and the representative ladder rungs φ⁵, φ⁸ are each
 131    pinned inside an explicit rational interval, entirely by choice-free integer
 132    arithmetic on ℤ[φ]. Every conjunct closes by `decide`, so the whole bundle
 133    lives in `{propext, Quot.sound}`. The real-side reading of these brackets is
 134    `DeltaSpine.GoldenIntReal.ladder_ratio_real_brackets` (sigma1). -/
 135theorem ladder_ratio_brackets :
 136    (RatLt 1618033 1000000 phi ∧ RatGt 1618034 1000000 phi) ∧
 137    (RatLt 1109 100 (phiPow 5) ∧ RatGt 1110 100 (phiPow 5)) ∧
 138    (RatLt 46978 1000 (phiPow 8) ∧ RatGt 46979 1000 (phiPow 8)) := by
 139  refine ⟨⟨phi_lower, phi_upper⟩, ⟨phi5_lower, phi5_upper⟩, ⟨phi8_lower, phi8_upper⟩⟩
 140
 141/-! ## Runtime certificates (`#eval`)
 142
 143These evaluate the same decidable predicates through the compiler, so the
 144rational bounds are confirmed by two independent engines (kernel + runtime).
 145They print `true`; `phiPow` prints its exact `⟨a, b⟩ = a + bφ` value. -/
 146
 147/-- info: true -/
 148#guard_msgs in
 149#eval decide (RatLt 1618033 1000000 phi)
 150
 151/-- info: true -/
 152#guard_msgs in
 153#eval decide (RatGt 1618034 1000000 phi)
 154
 155/-- info: true -/
 156#guard_msgs in
 157#eval decide (RatLt 1109 100 (phiPow 5))
 158
 159/-- info: true -/
 160#guard_msgs in
 161#eval decide (RatGt 1110 100 (phiPow 5))
 162
 163/-- info: true -/
 164#guard_msgs in
 165#eval decide (RatLt 46978 1000 (phiPow 8))
 166
 167/-- info: true -/
 168#guard_msgs in
 169#eval decide (RatGt 46979 1000 (phiPow 8))
 170
 171end GoldenInt
 172end DeltaSpine
 173end Foundation
 174end IndisputableMonolith
 175