IndisputableMonolith.Foundation.DeltaSpine.CostUniqueness

   1import IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
   2
   3/-!
   4# CostUniqueness: T5 on the φ-ladder, delta-forced (sigma0)
   5
   6**The choice-free re-derivation of the T5 cost-uniqueness node on its forced
   7discrete carrier.**
   8
   9The spine node `Cost.FunctionalEquation.law_of_logic_forces_jcost` proves T5
  10over `ℝ`: any reciprocal-symmetric, normalized, calibrated, continuous `F`
  11satisfying the Recognition Composition Law (RCL)
  12
  13    `F(xy) + F(x/y) = 2·F(x)·F(y) + 2·F(x) + 2·F(y)`
  14
  15equals `Jcost x = (x + x⁻¹)/2 − 1`. Its axiom closure is
  16`[propext, Classical.choice, Quot.sound]`: sigma1 (CHOICE).
  17
  18**The trichotomy read (2026-07-01)** classified that proof's continuum use:
  19the algebraic skeleton (substitute `x = e^s`, fold the RCL into d'Alembert's
  20`G(s+t) + G(s−t) = G(s)·G(t)` for `G = 2F + 2`) is pure instance leakage, and
  21the analytic core (the cosh ODE-uniqueness argument) exists only to exclude
  22pathological solutions that live on the *uncountable* domain `ℝ`. On the
  23domain the recognition ledger actually inhabits — the φ-ladder
  24`{φⁿ : n ∈ ℤ}` forced by T6 self-similarity — no pathology can exist: the
  25d'Alembert law is a two-step recurrence, and two initial values pin the whole
  26solution by induction. No continuity axis, no `Classical.choice`.
  27
  28This module carries that out over `GoldenInt = ℤ[φ]` (see
  29`DeltaSpine.GoldenInt`, the sigma0 T6 carrier):
  30
  311. `phiZpow n = φⁿ` through the unit group `GoldenIntˣ` (negative exponents
  32   are exact ring elements — `φ⁻¹ = φ − 1` — no division, no field).
  332. `traceZ n = φⁿ + φ⁻ⁿ`, the exact ℤ[φ] carrier of `2·cosh(n·log φ)`.
  343. `traceZ` satisfies d'Alembert `t(m+n) + t(m−n) = t(m)·t(n)` — a purely
  35   algebraic identity (existence).
  364. Any `h : ℤ → GoldenInt` satisfying d'Alembert with `h 0 = 2`,
  37   `h 1 = √5 = 2φ − 1` equals `traceZ` (uniqueness, by two-step strong
  38   induction; symmetry `h(−n) = h(n)` is *derived* from the law, not assumed).
  395. `Jdouble n = traceZ n − 2 = 2·J(φⁿ)` satisfies the exact discrete RCL
  40   `G(m+n) + G(m−n) = G(m)·G(n) + 2·G(m) + 2·G(n)` (the
  41   `SatisfiesCompositionLaw` shape with `x = φᵐ`, `y = φⁿ`), and is the
  42   unique such sequence with `G 0 = 0` (normalization) and
  43   `G 1 = √5 − 2 = 2φ − 3 = 2·J(φ)` (calibration). This is
  44   `t5_delta_forced`.
  45
  46**The doubled normalization.** `2` is not invertible in ℤ[φ], so the module
  47works with `2·J` throughout; the classical `J` is recovered at the display
  48boundary. With `G = 2F` the classical RCL
  49`F(xy) + F(x/y) = 2FxFy + 2Fx + 2Fy` becomes exactly
  50`G(xy) + G(x/y) = GxGy + 2Gx + 2Gy`, which is the `SatisfiesDiscreteRCL`
  51shape below — no content changes, only the scale.
  52
  53**Stronger hypotheses ledger than the classical node.** Classically T5 assumes
  54reciprocal symmetry (`IsReciprocalCost`), normalization, calibration, the RCL,
  55*and* continuity. Here the inputs are only normalization, calibration, and the
  56RCL: symmetry is a theorem (`dAlembert_symm`) and the continuity axis does not
  57exist on ℤ. The continuum tax — interpolating between the ladder rungs and
  58excluding discontinuous solutions of the real d'Alembert equation — is exactly
  59what remains sigma1, and it stays quarantined in `Cost.FunctionalEquation`
  60(and the display bridge `DeltaSpine.GoldenIntReal`:
  61`toReal (traceZ n) = 2·cosh (n·log φ)`).
  62
  63**Tactic hygiene** (same measured discipline as `DeltaSpine.GoldenInt`): no
  64full `simp`, no `omega` on goals with logical structure, case splits by
  65`rcases`, kernel `decide` on integer literals, `ring` over ℤ[φ] (probed
  66choice-free), and Mathlib's `Units`/`zpow` machinery (probed:
  67`[propext, Quot.sound]`).
  68
  69**Verdict target: sigma0 DELTA_FORCED** — every theorem here must close within
  70`{propext, Quot.sound}`. Audit with `scripts/sigma_audit.py` or
  71`#print axioms t5_delta_forced`.
  72
  73Delta Forcing Spectrum program: `Delta_Forcing_Spectrum_20260626.tex`.
  74-/
  75
  76namespace IndisputableMonolith
  77namespace Foundation
  78namespace DeltaSpine
  79namespace GoldenInt
  80
  81/-! ## Integer powers of φ through the unit group -/
  82
  83/-- The inverse of φ in ℤ[φ]: `φ⁻¹ = φ − 1 = ⟨−1, 1⟩`. Exact — no division. -/
  84def phiInv : GoldenInt := ⟨-1, 1⟩
  85
  86/-- `φ · φ⁻¹ = 1` — kernel computation. -/
  87theorem phi_mul_phiInv : phi * phiInv = 1 := by decide
  88
  89/-- `φ⁻¹ · φ = 1` — kernel computation. -/
  90theorem phiInv_mul_phi : phiInv * phi = 1 := by decide
  91
  92/-- The golden reciprocal identity `φ⁻¹ = φ − 1`, exact in ℤ[φ]. This is the
  93    self-similarity `φ² = φ + 1` read multiplicatively. -/
  94theorem phiInv_eq_phi_sub_one : phiInv = phi - 1 := by decide
  95
  96/-- φ as a unit of ℤ[φ]. -/
  97def phiUnit : GoldenIntˣ := ⟨phi, phiInv, phi_mul_phiInv, phiInv_mul_phi⟩
  98
  99/-- `φⁿ` for `n : ℤ`, through the unit group, so negative exponents are exact
 100    ring elements. -/
 101def phiZpow (n : ℤ) : GoldenInt := ((phiUnit ^ n : GoldenIntˣ) : GoldenInt)
 102
 103/-- The exponential law `φ^(m+n) = φ^m · φ^n`. -/
 104theorem phiZpow_add (m n : ℤ) : phiZpow (m + n) = phiZpow m * phiZpow n := by
 105  unfold phiZpow
 106  rw [zpow_add]
 107  rfl
 108
 109theorem phiZpow_zero : phiZpow 0 = 1 := by
 110  unfold phiZpow
 111  rw [zpow_zero]
 112  rfl
 113
 114theorem phiZpow_one : phiZpow 1 = phi := by
 115  unfold phiZpow
 116  rw [zpow_one]
 117  rfl
 118
 119theorem phiZpow_neg_one : phiZpow (-1) = phiInv := by
 120  unfold phiZpow
 121  rw [zpow_neg_one]
 122  rfl
 123
 124/-- `φ⁻ⁿ · φⁿ = 1`: every ladder rung is invertible. -/
 125theorem phiZpow_neg_mul (n : ℤ) : phiZpow (-n) * phiZpow n = 1 := by
 126  unfold phiZpow
 127  rw [← Units.val_mul, ← zpow_add, neg_add_cancel, zpow_zero, Units.val_one]
 128
 129/-! ## √5 and the trace sequence -/
 130
 131/-- `√5` as an exact element of ℤ[φ]: `√5 = 2φ − 1 = ⟨−1, 2⟩`. -/
 132def sqrtFive : GoldenInt := ⟨-1, 2⟩
 133
 134theorem sqrtFive_eq : sqrtFive = 2 * phi - 1 := by decide
 135
 136/-- `(√5)² = 5` — kernel computation, no `Real.sqrt`. -/
 137theorem sqrtFive_sq : sqrtFive * sqrtFive = 5 := by decide
 138
 139/-- The trace sequence `t(n) = φⁿ + φ⁻ⁿ`: the exact ℤ[φ] carrier of
 140    `2·cosh(n·log φ)`. -/
 141def traceZ (n : ℤ) : GoldenInt := phiZpow n + phiZpow (-n)
 142
 143theorem traceZ_zero : traceZ 0 = 2 := by
 144  unfold traceZ
 145  rw [neg_zero, phiZpow_zero]
 146  decide
 147
 148theorem traceZ_one : traceZ 1 = sqrtFive := by
 149  unfold traceZ
 150  rw [phiZpow_one, phiZpow_neg_one]
 151  decide
 152
 153/-- Reciprocal symmetry of the trace, by construction. -/
 154theorem traceZ_neg (n : ℤ) : traceZ (-n) = traceZ n := by
 155  unfold traceZ
 156  -- generic `neg_neg` on ℤ routes through a choice-tainted instance path;
 157  -- derive the identity by omega (atomic Int equality, choice-free)
 158  have e : -(-n) = n := by omega
 159  rw [e, add_comm]
 160
 161/-! ## The d'Alembert law: existence and uniqueness -/
 162
 163/-- The d'Alembert composition law on ℤ-indexed sequences:
 164    `h(m+n) + h(m−n) = h(m)·h(n)`. This is the `G`-side shape of
 165    `Cost.FunctionalEquation.composition_law_equiv_coshAdd`, discretized to
 166    the φ-ladder. -/
 167def SatisfiesDAlembert (h : ℤ → GoldenInt) : Prop :=
 168  ∀ m n : ℤ, h (m + n) + h (m - n) = h m * h n
 169
 170/-- **Existence**: the trace satisfies d'Alembert. A purely algebraic identity
 171    — expand both sides through the exponential law and `ring`. -/
 172theorem traceZ_dAlembert : SatisfiesDAlembert traceZ := by
 173  intro m n
 174  unfold traceZ
 175  have h1 : phiZpow (m + n) = phiZpow m * phiZpow n := phiZpow_add m n
 176  have h2 : phiZpow (-(m + n)) = phiZpow (-m) * phiZpow (-n) := by
 177    have e : -(m + n) = -m + -n := by ring
 178    rw [e, phiZpow_add]
 179  have h3 : phiZpow (m - n) = phiZpow m * phiZpow (-n) := by
 180    have e : m - n = m + -n := by ring
 181    rw [e, phiZpow_add]
 182  have h4 : phiZpow (-(m - n)) = phiZpow (-m) * phiZpow n := by
 183    have e : -(m - n) = -m + n := by ring
 184    rw [e, phiZpow_add]
 185  rw [h1, h2, h3, h4]
 186  ring
 187
 188/-- Reciprocal symmetry is **derived** from the law and normalization (the
 189    classical node has to assume it as `IsReciprocalCost`): put `m = 0` in
 190    d'Alembert and cancel. -/
 191theorem dAlembert_symm (h : ℤ → GoldenInt) (h0 : h 0 = 2)
 192    (hd : SatisfiesDAlembert h) : ∀ n : ℤ, h (-n) = h n := by
 193  intro n
 194  have hh := hd 0 n
 195  rw [zero_add, zero_sub, h0] at hh
 196  -- hh : h n + h (-n) = 2 * h n
 197  have h2 : h n + h (-n) = h n + h n := by rw [hh]; ring
 198  exact add_left_cancel h2
 199
 200/-- The two-step recurrence hiding in d'Alembert: put `n = 1`, so
 201    `h(k+2) = √5·h(k+1) − h(k)`. This is what replaces the cosh ODE on ℤ:
 202    a second-order recurrence needs exactly two initial values. -/
 203theorem dAlembert_step (h : ℤ → GoldenInt) (h1 : h 1 = sqrtFive)
 204    (hd : SatisfiesDAlembert h) (n : ℤ) :
 205    h (n + 2) = sqrtFive * h (n + 1) - h n := by
 206  have hh := hd (n + 1) 1
 207  have e1 : n + 1 + 1 = n + 2 := by ring
 208  have e2 : n + 1 - 1 = n := by ring
 209  rw [e1, e2, h1] at hh
 210  -- hh : h (n + 2) + h n = h (n + 1) * sqrtFive
 211  have h3 : h (n + 2) = h (n + 1) * sqrtFive - h n := eq_sub_of_add_eq hh
 212  rw [h3]; ring
 213
 214/-- The trace satisfies the recurrence (existence instantiated). -/
 215theorem traceZ_step (n : ℤ) :
 216    traceZ (n + 2) = sqrtFive * traceZ (n + 1) - traceZ n :=
 217  dAlembert_step traceZ traceZ_one traceZ_dAlembert n
 218
 219/-- **Uniqueness**: any sequence satisfying d'Alembert with the trace's two
 220    initial values *is* the trace. Two-step strong induction on ℕ, then the
 221    derived symmetry extends to all of ℤ. This is the sigma0 replacement for
 222    `ode_cosh_uniqueness_contdiff`: on the discrete carrier the recurrence
 223    leaves no room for pathological solutions, so no continuity hypothesis
 224    and no choice-dependent analysis are needed. -/
 225theorem dAlembert_unique (h : ℤ → GoldenInt)
 226    (h0 : h 0 = 2) (h1 : h 1 = sqrtFive)
 227    (hd : SatisfiesDAlembert h) :
 228    ∀ n : ℤ, h n = traceZ n := by
 229  have key : ∀ k : ℕ, h (k : ℤ) = traceZ (k : ℤ) := by
 230    intro k
 231    induction k using Nat.strong_induction_on with
 232    | _ k ih =>
 233      rcases k with _ | _ | k
 234      · show h 0 = traceZ 0
 235        rw [h0, traceZ_zero]
 236      · show h 1 = traceZ 1
 237        rw [h1, traceZ_one]
 238      · show h ((k + 2 : ℕ) : ℤ) = traceZ ((k + 2 : ℕ) : ℤ)
 239        have e2 : ((k + 2 : ℕ) : ℤ) = (k : ℤ) + 2 := by omega
 240        have e1 : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by omega
 241        have ihk : h (k : ℤ) = traceZ (k : ℤ) := ih k (by omega)
 242        have ihk1 : h ((k : ℤ) + 1) = traceZ ((k : ℤ) + 1) := by
 243          rw [← e1]
 244          exact ih (k + 1) (by omega)
 245        rw [e2, dAlembert_step h h1 hd, traceZ_step, ihk, ihk1]
 246  intro n
 247  rcases n with k | k
 248  · exact key k
 249  · have e : Int.negSucc k = -((k + 1 : ℕ) : ℤ) := rfl
 250    rw [e, dAlembert_symm h h0 hd, traceZ_neg]
 251    exact key (k + 1)
 252
 253/-! ## The J-cost form: the discrete Recognition Composition Law -/
 254
 255/-- The discrete RCL over ℤ[φ]: the exact shape of
 256    `Cost.FunctionalEquation.SatisfiesCompositionLaw` with `x = φᵐ`, `y = φⁿ`
 257    (so `x·y = φ^(m+n)`, `x/y = φ^(m−n)`), in the doubled normalization
 258    `G = 2F` that keeps everything inside the ring. -/
 259def SatisfiesDiscreteRCL (G : ℤ → GoldenInt) : Prop :=
 260  ∀ m n : ℤ, G (m + n) + G (m - n) = G m * G n + 2 * G m + 2 * G n
 261
 262/-- The doubled J-cost on the φ-ladder:
 263    `Jdouble n = φⁿ + φ⁻ⁿ − 2 = 2·J(φⁿ)` where `J(x) = (x + x⁻¹)/2 − 1`. -/
 264def Jdouble (n : ℤ) : GoldenInt := traceZ n - 2
 265
 266/-- Normalization: `2·J(φ⁰) = 2·J(1) = 0`. -/
 267theorem Jdouble_zero : Jdouble 0 = 0 := by
 268  unfold Jdouble
 269  rw [traceZ_zero]
 270  ring
 271
 272/-- Calibration: `2·J(φ) = φ + φ⁻¹ − 2 = √5 − 2 = 2φ − 3`. -/
 273theorem Jdouble_one : Jdouble 1 = sqrtFive - 2 := by
 274  unfold Jdouble
 275  rw [traceZ_one]
 276
 277/-- Reciprocal symmetry `2·J(φ⁻ⁿ) = 2·J(φⁿ)`, inherited from the trace. -/
 278theorem Jdouble_symm (n : ℤ) : Jdouble (-n) = Jdouble n := by
 279  unfold Jdouble
 280  rw [traceZ_neg]
 281
 282/-- **Existence**: the doubled J-cost satisfies the discrete RCL. Linear
 283    rearrangement of the d'Alembert identity. -/
 284theorem Jdouble_rcl : SatisfiesDiscreteRCL Jdouble := by
 285  intro m n
 286  unfold Jdouble
 287  have hd := traceZ_dAlembert m n
 288  have expand : (traceZ m - 2) * (traceZ n - 2) + 2 * (traceZ m - 2)
 289      + 2 * (traceZ n - 2) = traceZ m * traceZ n - 4 := by ring
 290  rw [expand, ← hd]
 291  ring
 292
 293/-- **Uniqueness**: any sequence satisfying the discrete RCL with the J-cost's
 294    normalization and calibration *is* the doubled J-cost. Shift by 2 into the
 295    d'Alembert frame and apply trace uniqueness. -/
 296theorem discreteRCL_unique (G : ℤ → GoldenInt)
 297    (hnorm : G 0 = 0)
 298    (hcalib : G 1 = sqrtFive - 2)
 299    (hcomp : SatisfiesDiscreteRCL G) :
 300    ∀ n : ℤ, G n = Jdouble n := by
 301  have h0 : (fun k : ℤ => G k + 2) 0 = 2 := by
 302    show G 0 + 2 = 2
 303    rw [hnorm]; ring
 304  have h1 : (fun k : ℤ => G k + 2) 1 = sqrtFive := by
 305    show G 1 + 2 = sqrtFive
 306    rw [hcalib]; ring
 307  have hd : SatisfiesDAlembert (fun k : ℤ => G k + 2) := by
 308    intro m n
 309    show G (m + n) + 2 + (G (m - n) + 2) = (G m + 2) * (G n + 2)
 310    have hc := hcomp m n
 311    have expand : (G m + 2) * (G n + 2)
 312        = G m * G n + 2 * G m + 2 * G n + 4 := by ring
 313    rw [expand, ← hc]
 314    ring
 315  have key := dAlembert_unique (fun k : ℤ => G k + 2) h0 h1 hd
 316  intro n
 317  have hk : G n + 2 = traceZ n := key n
 318  unfold Jdouble
 319  rw [← hk]
 320  ring
 321
 322/-! ## The T5 forcing theorem, delta-forced -/
 323
 324/-- **T5, DELTA-FORCED (sigma0)**: on the φ-ladder forced by T6, the doubled
 325    J-cost `Jdouble n = φⁿ + φ⁻ⁿ − 2 = 2·J(φⁿ)`
 326
 327    1. is normalized (`Jdouble 0 = 0`),
 328    2. is calibrated (`Jdouble 1 = √5 − 2 = 2·J(φ)`),
 329    3. is reciprocal-symmetric (**derived**, not assumed),
 330    4. satisfies the discrete Recognition Composition Law, and
 331    5. is the **unique** sequence doing so given only normalization,
 332       calibration, and the law.
 333
 334    This is the content of `law_of_logic_forces_jcost` restricted to the
 335    domain the ledger actually inhabits, with the continuum stripped away:
 336    no continuity hypothesis (the axis does not exist on ℤ), no reciprocity
 337    hypothesis (it is a theorem), no `Classical.choice` (audit:
 338    `{propext, Quot.sound}`). The remaining classical content — that among
 339    *continuous* interpolants of the ladder the cosh family is unique — is
 340    exactly the sigma1 residue quarantined in `Cost.FunctionalEquation`. -/
 341theorem t5_delta_forced :
 342    (Jdouble 0 = 0 ∧
 343     Jdouble 1 = sqrtFive - 2 ∧
 344     (∀ n : ℤ, Jdouble (-n) = Jdouble n) ∧
 345     SatisfiesDiscreteRCL Jdouble) ∧
 346    (∀ G : ℤ → GoldenInt,
 347      G 0 = 0 →
 348      G 1 = sqrtFive - 2 →
 349      SatisfiesDiscreteRCL G →
 350      ∀ n : ℤ, G n = Jdouble n) :=
 351  ⟨⟨Jdouble_zero, Jdouble_one, Jdouble_symm, Jdouble_rcl⟩, discreteRCL_unique⟩
 352
 353end GoldenInt
 354end DeltaSpine
 355end Foundation
 356end IndisputableMonolith
 357