Masses Mass Genesis T10 Rung Scalar Halving Wall Scalar Forced Eq Phi21 Of Banke

/-- **DERIVED: the rung scalar is `phi^21` (THEOREM, conditional on the banked
mass content).** Any positive rational-phi scalar whose deposit amplitude
squares to the banked `phi^42/8` is exactly `phi^21`; C9's rung-quantum
membership at `k = 21` is its instance. The exponent 21 is forced as half of
42. -/
theorem scalar_forced_eq_phi21_of_banked_mass {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q)
    (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ 42 / 8) :
    q = Constants.phi ^ 21 := by
  have h2 := (sqConsistent_scalar_eq_half_pow hq hq0 h).2
  rwa [show (42 : ℕ) / 2 = 21 from by norm_num] at h2

/-- **The upgrade (THEOREM).** Square-consistency forces the pure rung power:
if a positive rational-phi scalar's full-dimension deposit amplitude squares
to the mass content `phi^e / 8`, then `e` is even and the scalar is exactly
`phi^(e/2)`. The C9 rung-quantum shape is a CONSEQUENCE of the squaring on
`Q(phi)`, not an additional assumption. -/
theorem sqConsistent_scalar_eq_half_pow {q : ℝ} (hq : InQPhi q) (hq0 : 0 < q)
    {e : ℕ} (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) :
    Even e ∧ q = Constants.phi ^ (e / 2) := by
  have hsq : q ^ 2 = Constants.phi ^ e := (depositAmplitude_sq_eq_iff q e).mp h
  have heven : Even e := by
    by_contra hne
    exact not_sq_phi_pow_odd (Nat.not_even_iff_odd.mp hne) ⟨q, hq, hsq⟩
  refine ⟨heven, ?_⟩
  obtain ⟨m, hm⟩ := heven
  have hm2 : e / 2 = m := by omega
  have hm' : e = 2 * m := by omega
  rw [hm2]
  exact scalar_eq_half_pow_of_sq hq0.le (hm' ▸ hsq)

/-- **The parity obstruction (THEOREM).** No odd power of `phi` is a square
in the rational-phi field: if `x^2 = phi^e` with `x = p + q phi`, then
reading off coefficients against `phi^e = F_e phi + F_{e-1}` (banked
`phi_pow_fib`) gives `A = F_{e-1}`, `B = F_e`, and the norm identity forces
`N(x)^2 = F_{e-1}^2 + F_{e-1} F_e - F_e^2 = -1` by Cassini's identity
(`Int.fib_succ_mul_fib_pred_sub_fib_sq`) with `e` odd. No rational squares
to `-1`. -/
theorem not_sq_phi_pow_odd {e : ℕ} (he : Odd e) :
    ¬ ∃ x : ℝ, InQPhi x ∧ x ^ 2 = Constants.phi ^ e := by
  rintro ⟨x, ⟨p, q, hpq⟩, hx⟩
  have h1e : 1 ≤ e := by
    obtain ⟨k, hk⟩ := he
    omega
  have hshift : (Nat.fib (e + 1) : ℤ) - (Nat.fib e : ℤ) = (Nat.fib (e - 1) : ℤ) := by
    rcases e with _ | n
    · omega
    · rw [show n + 1 + 1 = n + 2 from rfl, Nat.fib_add_two, Nat.add_sub_cancel]
      push_cast
      ring
  have hfib1 : (Nat.fib (e + 1) : ℤ) = (Nat.fib e : ℤ) + (Nat.fib (e - 1) : ℤ) := by
    rcases e with _ | n
    · omega
    · rw [show n + 1 + 1 = n + 2 from rfl, Nat.fib_add_two, Nat.add_sub_cancel]
      push_cast
      ring
  rw [hpq, sq_rep p q] at hx
  rw [phi_pow_fib e] at hx
  push_cast at hx
  have hx' : ((p ^ 2 + q ^ 2 : ℚ) : ℝ) + ((2 * p * q + q ^ 2 : ℚ) : ℝ) * Constants.phi =
      (((Nat.fib (e + 1) : ℤ) - (Nat.fib e : ℤ) : ℚ) : ℝ) +
        (((Nat.fib e : ℤ) : ℚ) : ℝ) * Constants.phi := by
    push_cast
    linear_combination hx
  obtain ⟨hA, hB⟩ := rat_coeff_unique hx'
  have hn := phiNorm_sq p q
  rw [hA, hB] at hn
  have hshiftQ : ((Nat.fib (e + 1) : ℤ) : ℚ) - ((Nat.fib e : ℤ) : ℚ) =
      ((Nat.fib (e - 1) : ℤ) : ℚ) := by
    exact_mod_cast hshift
  rw [hshiftQ] at hn
  have hcass : (Nat.fib (e - 1) : ℤ) ^ 2 + (Nat.fib (e - 1) : ℤ) * (Nat.fib e : ℤ) -
      (Nat.fib e : ℤ) ^ 2 = (-1 : ℤ) := by
    have h0 := Int.fib_succ_mul_fib_pred_sub_fib_sq (e : ℤ)
    have he1 : (e : ℤ) + 1 = ((e + 1 : ℕ) : ℤ) := by push_cast; ring
    have he2 : (e : ℤ) - 1 = ((e - 1 : ℕ) : ℤ) := by
      rcases e with _ | n
      · omega
      · rw [Nat.add_sub_cancel]
        push_cast
        ring
    rw [he1, he2, Int.fib_natCast, Int.fib_natCast, Int.fib_natCast,
      Int.natAbs_natCast, Odd.neg_one_pow he] at h0
    rw [hfib1] at h0
    linear_combination h0
  have hcassQ : ((Nat.fib (e - 1) : ℤ) : ℚ) ^ 2 +
      ((Nat.fib (e - 1) : ℤ) : ℚ) * ((Nat.fib e : ℤ) : ℚ) -
        ((Nat.fib e : ℤ) : ℚ) ^ 2 = (-1 : ℚ) := by
    exact_mod_cast hcass
  have hnorm : (p ^ 2 + p * q - q ^ 2 : ℚ) ^ 2 = (-1 : ℚ) := by
    rw [hn]
    linear_combination hcassQ
  have hnonneg : (0 : ℚ) ≤ (p ^ 2 + p * q - q ^ 2) ^ 2 := sq_nonneg _
  rw [hnorm] at hnonneg
  norm_num at hnonneg

/-- **Parity constraint on the yardstick (THEOREM).** If the genesis deposit
has a rational-phi scalar at mass exponent `e = r0(EW) - 13`, the
electroweak yardstick is ODD. The frozen 55 passes; an even yardstick such
as 56 is excluded. The first theorem-tier constraint on the yardstick beyond
the gauge sum. -/
theorem odd_yardstick_of_sqConsistent_genesis {q : ℝ} (hq : InQPhi q) {e : ℕ}
    (hr : Anchor.r0 Anchor.Sector.Electroweak = (e : ℤ) + 13)
    (h : (q * creationDepositNorm) ^ 2 = Constants.phi ^ e / 8) :
    Odd (Anchor.r0 Anchor.Sector.Electroweak) := by
  have he := even_mass_exponent_of_sqConsistent hq h
  rw [hr]
  obtain ⟨m, hm⟩ := he
  use (m : ℤ) + 6
  omega

/-- **No modular-flow predicate can fix the absolute scale (THEOREM).** Any
predicate of the modular eigenvalue function accepts an amplitude iff it
accepts every nonzero rescale, so the class of modular-flow scalar laws
cannot distinguish `phi^21` from `phi^20` (or any other rescaling) in the
deposit prefactor. This closes the C10 lead (ii) route through the tower's
modular spectrum. -/
theorem modularFlow_predicate_scale_blind {N : ℕ} (k : Fin N)
    (P : (SectorN N → SectorN N → ℝ) → Prop) {a b : ℝ} (ha : a ≠ 0) (hb : b ≠ 0) :
    P (modularEigenvalueN a k) ↔ P (modularEigenvalueN b k) := by
  have hfun : modularEigenvalueN a k = modularEigenvalueN b k := by
    funext i j
    exact modularEigenvalueN_amplitude_blind ha hb k i j
  rw [hfun]