/-
  StringTheoryQLF.lean
  Quantum Logical Framework — String Theory via Gauge-Fold Depth

  Two central claims:

  1. "Infinities relate to folds":
     The infinite tower of string excitation levels corresponds to the infinite
     hierarchy of gauge-fold depths in the RhoProcess algebra.  Each level n is a
     well-typed ZFA-stable Hermitian RhoProcess.  The infinity is tame — it is the
     possibilist infinity of admissible logical closures, not a UV divergence.

  2. "Modes to ways it can happen":
     The number of distinct string modes at excitation level n equals the number of
     ZFA-stable strings of length 2n: exactly C(2n,n), proved by
     find_stable_states_length_even in QLF_Riemann.lean.  The string mode-degeneracy
     at each mass level is not a free parameter — it is forced by ZFA balance.

  Key results proved here:
  • GaugeFoldPair: the fundamental QLF building block for closed strings
  • ClosedStringLevel f n: the n-th excitation (n fold-pairs in parallel)
  • string_mass_spectrum: eval at level n = n • (f.toMatrix + f.toMatrix)
  • string_level_zfa_stable / string_level_hermitian: tower is ZFA-stable + Hermitian
  • string_mode_count: modes at level n = C(2n,n)  [from find_stable_states_length_even]
  • compactification_zfa_stable: extra Form dimensions preserve ZFA closure
  • landscape_zfa_stable: every (Form, level) pair is a valid ZFA sector

  Author: Jim Scarver + Claude — May 2026
-/

import RhoQuCalc     -- RhoProcess, eval, Form, toTopoString, ZFA theorems
import QLF_Riemann   -- find_stable_states_length_even, find_stable_states

open Matrix

/-! ## Gauge-fold pair: fundamental closed string mode -/

/-- One gauge-fold pair: the QLF building block of a closed string mode.
    `action f` enters a logical state; `lift f` closes the loop back.
    Together they form a Hermitian equilibrium pair — the ZFA-closed analog of
    a closed string at its ground vibrational mode. -/
def GaugeFoldPair (f : Form) : RhoProcess :=
  RhoProcess.parallel (RhoProcess.action f) (RhoProcess.lift f)

/-- The gauge-fold pair is Hermitian (bosonic equilibrium ground mode) -/
theorem gaugeFoldPair_hermitian (f : Form) :
    (GaugeFoldPair f).eval.IsHermitian :=
  RhoProcess.action_lift_hermitian f

/-- Eval of a gauge-fold pair: action + lift = f.toMatrix + f.toMatrix
    (since f.toMatrix is Hermitian: f.toMatrix† = f.toMatrix) -/
theorem gaugeFoldPair_eval (f : Form) :
    (GaugeFoldPair f).eval = f.toMatrix + f.toMatrix := by
  simp [GaugeFoldPair, RhoProcess.eval, Form.toMatrix_adjoint]

/-! ## Closed string excitation tower -/

/-- The n-th closed string excitation level: n gauge-fold pairs in parallel.
    Level 0 is the vacuum (zero process); each step adds one gauge fold.
    The tower n ↦ ClosedStringLevel f n is infinite and well-typed:
    this is the QLF resolution of the "infinite string tower" — a tame possibilist
    infinity, not a UV divergence. -/
def ClosedStringLevel (f : Form) : ℕ → RhoProcess
  | 0     => RhoProcess.zero
  | n + 1 => RhoProcess.parallel (ClosedStringLevel f n) (GaugeFoldPair f)

/-- Level 0 is the vacuum: eval = 0 -/
@[simp] theorem closedString_zero_eval (f : Form) :
    (ClosedStringLevel f 0).eval = 0 := by
  simp [ClosedStringLevel, RhoProcess.eval]

/-- Each step adds one fold-pair matrix to the eval -/
theorem closedString_succ_eval (f : Form) (n : ℕ) :
    (ClosedStringLevel f (n + 1)).eval =
    (ClosedStringLevel f n).eval + (f.toMatrix + f.toMatrix) := by
  simp [ClosedStringLevel, RhoProcess.eval, gaugeFoldPair_eval]

/-- **String mass spectrum**: eval at level n = n copies of the fold-pair matrix.
    QLF analog of M² ∝ N in standard string theory: each gauge fold adds one unit
    of mass/excitation. -/
theorem string_mass_spectrum (f : Form) (n : ℕ) :
    (ClosedStringLevel f n).eval = n • (f.toMatrix + f.toMatrix) := by
  induction n with
  | zero => simp
  | succ n ih => rw [closedString_succ_eval, ih, succ_nsmul]

/-! ## ZFA stability and Hermitian structure -/

/-- Every string level is ZFA-stable.
    "Infinities relate to folds": the ∞ of modes is the ∞ of gauge-fold depths,
    each individually ZFA-closed and physically admissible.
    No renormalization or UV cutoff needed — ZFA already prunes non-terminating histories. -/
theorem string_level_zfa_stable (f : Form) (n : ℕ) :
    achieves_ZFA (toTopoString (ClosedStringLevel f n)) :=
  RhoProcess.rho_process_always_zfa _

/-- Every string level has a symmetric TopoString (lies on the critical line) -/
theorem string_level_symmetric (f : Form) (n : ℕ) :
    is_symmetric (toTopoString (ClosedStringLevel f n)) :=
  RhoProcess.rho_process_always_symmetric _

/-- Every string level is Hermitian -/
theorem string_level_hermitian (f : Form) (n : ℕ) :
    (ClosedStringLevel f n).eval.IsHermitian := by
  induction n with
  | zero =>
    simp only [ClosedStringLevel, RhoProcess.eval]
    simp [Matrix.IsHermitian]
  | succ n ih =>
    simp only [ClosedStringLevel]
    exact RhoProcess.parallel_hermitian _ _ ih (gaugeFoldPair_hermitian f)

/-! ## Modes to ways it can happen -/

/-- **String mode count**: the number of distinct string modes at excitation depth 2n
    is exactly C(2n,n).

    "Modes to ways it can happen": at mass level n, the string can be excited in
    C(2n,n) distinct ZFA-balanced ways — the number of balanced phase strings of
    length 2n from find_stable_states_length_even.

    This connects the string degeneracy problem directly to the QLF combinatorial core:
    the mode count at each level is not a free parameter but is fixed by ZFA balance,
    the same constraint that drives the QLF Riemann program. -/
theorem string_mode_count (n : ℕ) :
    (find_stable_states (2 * n)).length = Nat.choose (2 * n) n :=
  QLF.find_stable_states_length_even n

/-- The list of distinct string modes at excitation level n -/
def stringModesAtLevel (n : ℕ) : List TopoString :=
  find_stable_states (2 * n)

/-- Mode count is C(2n,n) ≈ 4^n / √(πn) — consistent with exponential (Hagedorn) growth -/
theorem string_modes_count_eq_choose (n : ℕ) :
    (stringModesAtLevel n).length = Nat.choose (2 * n) n :=
  QLF.find_stable_states_length_even n

/-- Every mode in the list is ZFA-stable (all elements of find_stable_states are ZFA-closed) -/
theorem string_modes_all_zfa (n : ℕ) (s : TopoString) (hs : s ∈ stringModesAtLevel n) :
    achieves_ZFA s := by
  simp only [stringModesAtLevel] at hs
  obtain ⟨_, hpure, hsym⟩ := (QLF.find_stable_states_iff (2 * n) s).mp hs
  exact phase_symmetric_achieves_zfa s hpure hsym

/-! ## Compactification -/

/-- Superpose two Forms to represent compactified extra dimensions.
    The extra Form components encode the compact manifold degrees of freedom. -/
def compactifyForm (base extra : Form) : Form :=
  { t := base.t + extra.t
    x := base.x + extra.x
    y := base.y + extra.y
    z := base.z + extra.z }

/-- Compactification preserves ZFA stability: extra Form dimensions are always admissible -/
theorem compactification_zfa_stable (base extra : Form) (n : ℕ) :
    achieves_ZFA (toTopoString (ClosedStringLevel (compactifyForm base extra) n)) :=
  RhoProcess.rho_process_always_zfa _

/-- Compactified mass spectrum: eval = n • (M_compact + M_compact) -/
theorem compactification_mass_spectrum (base extra : Form) (n : ℕ) :
    (ClosedStringLevel (compactifyForm base extra) n).eval =
    n • ((compactifyForm base extra).toMatrix + (compactifyForm base extra).toMatrix) :=
  string_mass_spectrum _ n

/-! ## The string landscape -/

/-- The string landscape: all pairs (Form, excitation level).
    Each element is a ZFA-stable RhoProcess sector. -/
def StringLandscape : Type := Form × ℕ

/-- Every landscape element is ZFA-stable -/
theorem landscape_zfa_stable (s : StringLandscape) :
    achieves_ZFA (toTopoString (ClosedStringLevel s.1 s.2)) :=
  string_level_zfa_stable s.1 s.2

/-- Every landscape element lies on the critical line -/
theorem landscape_on_critical_line (s : StringLandscape) :
    is_symmetric (toTopoString (ClosedStringLevel s.1 s.2)) :=
  string_level_symmetric s.1 s.2

/-- The mode count is C(2n,n) for every landscape level -/
theorem landscape_mode_count (s : StringLandscape) :
    (stringModesAtLevel s.2).length = Nat.choose (2 * s.2) s.2 :=
  string_modes_count_eq_choose s.2