IndisputableMonolith.Constants.AlphaGenesis.PatternForcing

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Constants.GapWeight.Formula
   4import IndisputableMonolith.Foundation.MeasureForcing
   5
   6/-!
   7# Alpha Genesis M2: Pattern Forcing
   8
   9**THE THEOREM.** The φ-pattern `u_t = φᵗ` consumed by the w₈ spectral
  10projection is not a choice. Any eight-tick ladder pattern with unit base,
  11constant positive step ratio, and self-similar ratio (`r² = r + 1`, the T6
  12equation) is exactly `φᵗ`. And the decay envelope `φ⁻ᵏ` inside the spectral
  13weight is the T9 forced measure itself, term for term.
  14
  15This discharges discrete choice (ii) of the no-fit proposition (the
  16"canonical φ-pattern" choice): the pattern is forced by T6 self-similarity
  17given the T7 carrier, and its conjugate envelope is the unique forced
  18measure of `Foundation.MeasureForcing`.
  19
  20## The reciprocity structure
  21
  22The w₈ machinery consumes two φ-structures:
  23
  24* the time-domain pattern `φᵗ` (growth display), and
  25* the spectral decay envelope `φ⁻ᵏ` (weight display).
  26
  27These are reciprocal displays of ONE object: `pattern · forcedMeasure = 1`
  28tick by tick (`pattern_mul_forced_measure`). The reciprocity is the ledger's
  29J-symmetry (`J(x) = J(1/x)`): cost-side and weight-side displays are
  30conjugate. Neither is an independent input.
  31
  32STATUS: THEOREM (0 sorry target). No CODATA reference anywhere in this file.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Constants
  37namespace AlphaGenesis
  38
  39noncomputable section
  40
  41/-- The unique positive root of the self-similarity equation `x² = x + 1`
  42is φ. (Self-contained; the T6 forcing equation.) -/
  43theorem pos_root_eq_phi {r : ℝ} (hr : 0 < r) (hsq : r ^ 2 = r + 1) :
  44    r = Constants.phi := by
  45  have h5 : (2 * r - 1) ^ 2 = 5 := by nlinarith [hsq]
  46  have hge : 0 ≤ 2 * r - 1 := by
  47    by_contra hneg
  48    push_neg at hneg
  49    have h2 : (2 * r - 1 + 1) * (1 - (2 * r - 1)) = 1 - (2 * r - 1) ^ 2 := by ring
  50    have h3 : 0 < (2 * r - 1 + 1) * (1 - (2 * r - 1)) := by
  51      apply mul_pos
  52      · linarith
  53      · linarith
  54    rw [h2, h5] at h3
  55    norm_num at h3
  56  have hsqrt : Real.sqrt 5 = 2 * r - 1 := by
  57    rw [show (5 : ℝ) = (2 * r - 1) ^ 2 from h5.symm]
  58    exact Real.sqrt_sq hge
  59  have hphi : Constants.phi = (1 + Real.sqrt 5) / 2 := rfl
  60  rw [hphi, hsqrt]
  61  ring
  62
  63/-- An **eight-tick ladder pattern**: unit base, constant positive step
  64ratio, ratio self-similar (the T6 equation `r² = r + 1`). The carrier is the
  65T7 eight-tick window (indexed by ℕ, consumed at `Fin 8`). -/
  66structure EightTickLadder where
  67  /-- The pattern values. -/
  68  u : ℕ → ℝ
  69  /-- Unit base: the pattern starts at the identity ratio. -/
  70  base : u 0 = 1
  71  /-- The constant step ratio. -/
  72  ratio : ℝ
  73  /-- The ratio is positive. -/
  74  ratio_pos : 0 < ratio
  75  /-- Constant-ratio recurrence. -/
  76  step : ∀ n, u (n + 1) = ratio * u n
  77  /-- Self-similarity (T6): the ratio satisfies `r² = r + 1`. -/
  78  self_similar : ratio ^ 2 = ratio + 1
  79
  80namespace EightTickLadder
  81
  82/-- The ratio of any eight-tick ladder is φ. -/
  83theorem ratio_eq_phi (L : EightTickLadder) : L.ratio = Constants.phi :=
  84  pos_root_eq_phi L.ratio_pos L.self_similar
  85
  86/-- **PATTERN FORCING.** Every eight-tick ladder is the φ-pattern. -/
  87theorem pattern_forced (L : EightTickLadder) : ∀ n, L.u n = Constants.phi ^ n := by
  88  intro n
  89  induction n with
  90  | zero => simpa using L.base
  91  | succ k ih =>
  92      rw [L.step k, ih, L.ratio_eq_phi]
  93      ring
  94
  95end EightTickLadder
  96
  97/-- The canonical ladder (non-vacuity witness). -/
  98def canonicalLadder : EightTickLadder where
  99  u := fun n => Constants.phi ^ n
 100  base := by norm_num
 101  ratio := Constants.phi
 102  ratio_pos := Constants.phi_pos
 103  step := fun n => by ring
 104  self_similar := Constants.phi_sq_eq
 105
 106/-- The GapWeight pattern is the forced ladder restricted to the 8-tick
 107window: `phiPattern t = L.u t` for EVERY admissible ladder L. -/
 108theorem phiPattern_is_forced (L : EightTickLadder) (t : Fin 8) :
 109    GapWeight.phiPattern t = L.u t.val := by
 110  rw [L.pattern_forced]
 111  rfl
 112
 113/-- **RECIPROCITY.** The time-domain pattern and the T9 forced measure are
 114reciprocal displays: `φᵗ · w(t) = 1` at every tick. The growth pattern is
 115the J-conjugate of the unique forced measure; neither is an independent
 116input. -/
 117theorem pattern_mul_forced_measure (t : Fin 8) :
 118    GapWeight.phiPattern t * Foundation.MeasureForcing.latticeWeight t.val = 1 := by
 119  show Constants.phi ^ t.val * (1 / Constants.phi) ^ t.val = 1
 120  rw [one_div, ← mul_pow, mul_inv_cancel₀ Constants.phi_ne_zero, one_pow]
 121
 122/-- **ENVELOPE IDENTITY.** The decay envelope inside the spectral weight IS
 123the forced measure: `geometricWeight k = sin²(kπ/8) · latticeWeight k` for
 124every nonzero mode. The `φ⁻ᵏ` in w₈ is not an α-specific choice; it is the
 125unique T9 recognition weight. -/
 126theorem geometricWeight_eq_sin_mul_forced_measure (k : Fin 8) (hk : ¬ k.val = 0) :
 127    GapWeight.geometricWeight k =
 128      (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 *
 129        Foundation.MeasureForcing.latticeWeight k.val := by
 130  simp only [GapWeight.geometricWeight, if_neg hk]
 131  show (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 * Constants.phi ^ (-(k.val : ℤ)) =
 132    (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 * (1 / Constants.phi) ^ k.val
 133  congr 1
 134  rw [zpow_neg, zpow_natCast, one_div, inv_pow]
 135
 136/-- **PATTERN FORCING CERTIFICATE.** Bundles the M2 closure:
 1371. every admissible ladder is `φᵗ` (the pattern is forced, not chosen);
 1382. the GapWeight pattern is that forced ladder;
 1393. pattern and forced measure are reciprocal displays;
 1404. the spectral decay envelope is the forced measure. -/
 141structure PatternForcingCert where
 142  deriving Inhabited
 143
 144@[simp] def PatternForcingCert.verified (_c : PatternForcingCert) : Prop :=
 145  (∀ (L : EightTickLadder) (n : ℕ), L.u n = Constants.phi ^ n) ∧
 146  (∀ (L : EightTickLadder) (t : Fin 8), GapWeight.phiPattern t = L.u t.val) ∧
 147  (∀ t : Fin 8,
 148    GapWeight.phiPattern t * Foundation.MeasureForcing.latticeWeight t.val = 1) ∧
 149  (∀ k : Fin 8, ¬ k.val = 0 →
 150    GapWeight.geometricWeight k =
 151      (Real.sin ((k.val : ℝ) * Real.pi / 8)) ^ 2 *
 152        Foundation.MeasureForcing.latticeWeight k.val)
 153
 154theorem PatternForcingCert.verified_any (c : PatternForcingCert) :
 155    PatternForcingCert.verified c := by
 156  refine ⟨?_, ?_, ?_, ?_⟩
 157  · intro L n
 158    exact L.pattern_forced n
 159  · intro L t
 160    exact phiPattern_is_forced L t
 161  · exact pattern_mul_forced_measure
 162  · exact geometricWeight_eq_sin_mul_forced_measure
 163
 164end
 165
 166end AlphaGenesis
 167end Constants
 168end IndisputableMonolith
 169