IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolSpecificationAudit

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTSymbolPreflight
   2
   3/-!
   4# Regge TT symbol specification audit: scaling well-posedness of the `-1/4` target
   5
   6QG full-theory campaign, `ReggeTTContinuumSymbol` program, Crux-1(c) lane,
   7Gate A0 of the panel-locked protocol "Normalization-Gated Schläfli Two-Jet".
   8
   9## What this gate decides
  10
  11The OPEN target `ReggeTTContinuumIsotropyTarget` claims a FIXED value
  12`-(1/4)` for the continuum TT Bloch symbol on every TT polarization.  A
  13fixed numerical value is meaningful only if the statement cannot be
  14rescaled into a contradiction: the plane-wave family
  15`ℓ_e(t) = ℓ²_flat + t · c_d(E) · cos(k·x_mid)` is linear in the
  16polarization matrix `E` through the edge-class coefficient
  17`c_d(E) = Σ_ij E_ij D_d^i D_d^j`, so replacing `E ↦ c·E` reparametrizes
  18the SAME family (`t ↦ c·t`), and the second-difference quadratic form must
  19scale by `c²`.  This module kernel-checks exactly that scaling chain and
  20the normalization pin that makes the fixed-value statement well-posed.
  21
  22## Convention-consistency audit (documentation record, checked by hand
  23against the kernel definitions in `ReggeTTSymbolPreflight`)
  24
  25* `polEdgeCoeff E d = Σ_{i,j} E_ij · D_d^i · D_d^j` sums over ALL ordered
  26  index pairs, so for symmetric `E` each off-diagonal pair `(i,j) ≠ (j,i)`
  27  contributes twice.  This is the standard quadratic-form convention
  28  `D^T E D`.
  29* The Frobenius normalization in `IsTTPolarization` (fourth conjunct,
  30  `Σ_{i,j} E_ij · E_ij = 1`) likewise sums over ALL ordered pairs.
  31* The C10 numerics probe (`state/qg_full_theory/true_regge_tt_probe/`,
  32  commit f1d44266e5) used these same two conventions (background record;
  33  NUMERICAL EVIDENCE, never proof).
  34* Conclusion of the audit: the two double-counting conventions are
  35  CONSISTENT with each other; no mismatch was found, so the lane
  36  proceeds.  The kernel content below shows the target statement is
  37  scaling-coherent: the symbol value scales as `c²` under `E ↦ c·E`
  38  (`TTBlochSymbolIs_smul`), and `IsTTPolarization` pins the Frobenius
  39  norm so the only rescalings preserving the hypothesis class are
  40  `c² = 1` (`isTTPolarization_smul_iff`), under which `c²·H = H`.  Hence
  41  quantifying a FIXED value over `IsTTPolarization` is well-posed, while
  42  an unnormalized fixed-value claim would be contradictory.
  43
  44## Tier tags
  45
  46* THEOREM: every named result in this file (kernel-checked; no sorry, no
  47  admit, no new axioms, no `native_decide`, no `: True` shells).  All
  48  results here are pure algebra/topology over the preflight definitions
  49  and carry the standard axiom footprint
  50  `[propext, Classical.choice, Quot.sound]` (they do not touch the
  51  certified angle-sum chain, so no `Lean.ofReduceBool`/`Lean.trustCompiler`).
  52* No claim about the VALUE `-1/4` is made or implied anywhere here; the
  53  continuum target stays OPEN and its status flag stays `false`.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Gravity
  58namespace Analysis
  59namespace ReggeTTSymbolSpecificationAudit
  60
  61open ReggeTTSymbolPreflight
  62
  63noncomputable section
  64
  65variable (N : ℕ) [NeZero N]
  66
  67/-! ## §1. Scaling of the edge-class coefficient (Gate A0(a)) -/
  68
  69/-- (a) THEOREM: the edge-class coefficient is linear in the polarization,
  70entrywise-scaling form. -/
  71theorem polEdgeCoeff_mul_left (c : ℝ) (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
  72    polEdgeCoeff (fun i j => c * E i j) d = c * polEdgeCoeff E d := by
  73  unfold polEdgeCoeff
  74  rw [Finset.mul_sum]
  75  refine Finset.sum_congr rfl fun i _ => ?_
  76  rw [Finset.mul_sum]
  77  refine Finset.sum_congr rfl fun j _ => ?_
  78  ring
  79
  80/-- The scalar action on polarization matrices is entrywise. -/
  81theorem smul_polarization_apply (c : ℝ) (E : Fin 3 → Fin 3 → ℝ) (i j : Fin 3) :
  82    (c • E) i j = c * E i j := rfl
  83
  84/-- (a) THEOREM, `•` form: `polEdgeCoeff (c • E) d = c * polEdgeCoeff E d`. -/
  85theorem polEdgeCoeff_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ) (d : Fin 7) :
  86    polEdgeCoeff (c • E) d = c * polEdgeCoeff E d := by
  87  have h : (c • E) = fun i j => c * E i j := rfl
  88  rw [h]
  89  exact polEdgeCoeff_mul_left c E d
  90
  91/-! ## §2. Scaling of the plane-wave family (Gate A0(b)) -/
  92
  93/-- (b) THEOREM: rescaling the polarization by `c` reparametrizes the SAME
  94plane-wave edge-field family by `t ↦ c·t`.  This is the exact sense in
  95which the polarization normalization and the amplitude normalization are
  96one and the same gauge. -/
  97theorem planeWaveEdgeField_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ)
  98    (k : Fin 3 → ℝ) (t : ℝ) :
  99    planeWaveEdgeField N (c • E) k t = planeWaveEdgeField N E k (c * t) := by
 100  funext e
 101  simp only [planeWaveEdgeField, polEdgeCoeff_smul]
 102  ring
 103
 104/-- (b) corollary: the action profile of the rescaled polarization is the
 105original profile at the rescaled amplitude. -/
 106theorem planeWaveActionProfile_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ)
 107    (k : Fin 3 → ℝ) (t : ℝ) :
 108    planeWaveActionProfile N (c • E) k t =
 109      planeWaveActionProfile N E k (c * t) := by
 110  unfold planeWaveActionProfile
 111  rw [planeWaveEdgeField_smul]
 112
 113/-! ## §3. Quadratic scaling of the second-difference form (Gate A0(c)) -/
 114
 115/-- (c) THEOREM: under `E ↦ c·E` the second-difference quadratic form
 116scales QUADRATICALLY, `D_{cE}(t) = c² · D_E(c·t)`.  This is the kernel
 117fact that makes any unnormalized "fixed `-1/4`" claim contradictory: the
 118same physical family would have to report both `H` and `c²·H`. -/
 119theorem ttSecondDifference_smul {c t : ℝ} (hc : c ≠ 0) (ht : t ≠ 0)
 120    (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ) :
 121    ttSecondDifference N (c • E) k t =
 122      c ^ 2 * ttSecondDifference N E k (c * t) := by
 123  have hN : ((N : ℝ)) ≠ 0 := Nat.cast_ne_zero.mpr (NeZero.ne N)
 124  unfold ttSecondDifference
 125  simp only [planeWaveActionProfile_smul, mul_zero, mul_neg]
 126  field_simp
 127
 128/-! ## §4. Scaling of the Bloch symbol value predicate (Gate A0(d)) -/
 129
 130/-- Multiplication by a nonzero constant maps the punctured neighborhood
 131filter of `0` to itself. -/
 132theorem tendsto_const_mul_punctured {c : ℝ} (hc : c ≠ 0) :
 133    Filter.Tendsto (fun t : ℝ => c * t)
 134      (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhdsWithin 0 {(0 : ℝ)}ᶜ) := by
 135  have h1 : Filter.Tendsto (fun t : ℝ => c * t) (nhds 0) (nhds 0) := by
 136    simpa using (continuous_const.mul continuous_id).tendsto (0 : ℝ)
 137  refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
 138    (h1.mono_left nhdsWithin_le_nhds) ?_
 139  filter_upwards [self_mem_nhdsWithin] with t ht
 140  have ht' : t ≠ 0 := ht
 141  exact mul_ne_zero hc ht'
 142
 143/-- One direction of (d): if the symbol value at `E` is `H`, the symbol
 144value at `c • E` is `c² · H`. -/
 145theorem TTBlochSymbolIs_smul_of {c : ℝ} (hc : c ≠ 0)
 146    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) (H : ℝ)
 147    (h : TTBlochSymbolIs N E m H) :
 148    TTBlochSymbolIs N (c • E) m (c ^ 2 * H) := by
 149  unfold TTBlochSymbolIs at h ⊢
 150  have hcomp := h.comp (tendsto_const_mul_punctured hc)
 151  have hmul := hcomp.const_mul (c ^ 2)
 152  refine hmul.congr' ?_
 153  filter_upwards [self_mem_nhdsWithin] with t ht
 154  have ht' : t ≠ 0 := ht
 155  exact (ttSecondDifference_smul N hc ht' E (commensurateMomentum N m)).symm
 156
 157/-- (d) THEOREM: the Bloch symbol value predicate transforms exactly
 158quadratically under polarization rescaling, as an equivalence.  Any
 159well-posed fixed-value target must therefore fix the polarization
 160normalization; `IsTTPolarization` does (§5). -/
 161theorem TTBlochSymbolIs_smul {c : ℝ} (hc : c ≠ 0)
 162    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) (H : ℝ) :
 163    TTBlochSymbolIs N E m H ↔ TTBlochSymbolIs N (c • E) m (c ^ 2 * H) := by
 164  constructor
 165  · exact TTBlochSymbolIs_smul_of N hc E m H
 166  · intro h
 167    have hc' : c⁻¹ ≠ 0 := inv_ne_zero hc
 168    have h' := TTBlochSymbolIs_smul_of N hc' (c • E) m (c ^ 2 * H) h
 169    have hE : c⁻¹ • c • E = E := by
 170      rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
 171    have hH : (c⁻¹) ^ 2 * (c ^ 2 * H) = H := by
 172      field_simp
 173    rwa [hE, hH] at h'
 174
 175/-! ## §5. The normalization pin and statement well-posedness (Gate A0(e)) -/
 176
 177/-- Frobenius square-sum of a polarization matrix (ordered-pair
 178convention, matching both `polEdgeCoeff` and `IsTTPolarization`). -/
 179def frobeniusSq (E : Fin 3 → Fin 3 → ℝ) : ℝ :=
 180  ∑ i : Fin 3, ∑ j : Fin 3, E i j * E i j
 181
 182/-- (e), pin re-export: `IsTTPolarization` pins the Frobenius square-sum
 183to `1` (fourth conjunct of the definition). -/
 184theorem isTTPolarization_frobenius_pinned (m : Fin 3 → ℤ)
 185    (E : Fin 3 → Fin 3 → ℝ) (h : IsTTPolarization m E) :
 186    frobeniusSq E = 1 :=
 187  h.2.2.2
 188
 189/-- The Frobenius square-sum scales quadratically under `E ↦ c·E`. -/
 190theorem frobeniusSq_smul (c : ℝ) (E : Fin 3 → Fin 3 → ℝ) :
 191    frobeniusSq (c • E) = c ^ 2 * frobeniusSq E := by
 192  unfold frobeniusSq
 193  rw [Finset.mul_sum]
 194  refine Finset.sum_congr rfl fun i _ => ?_
 195  rw [Finset.mul_sum]
 196  refine Finset.sum_congr rfl fun j _ => ?_
 197  show (c * E i j) * (c * E i j) = c ^ 2 * (E i j * E i j)
 198  ring
 199
 200/-- (e) THEOREM, the pin is real: starting from a TT polarization `E`, the
 201rescaled matrix `c • E` remains a TT polarization exactly when `c² = 1`.
 202Symmetry, tracelessness, and transversality survive every rescaling; the
 203Frobenius pin is the ONLY normalization-fixing clause, and it works. -/
 204theorem isTTPolarization_smul_iff (m : Fin 3 → ℤ)
 205    (E : Fin 3 → Fin 3 → ℝ) (c : ℝ) (h : IsTTPolarization m E) :
 206    IsTTPolarization m (c • E) ↔ c ^ 2 = 1 := by
 207  obtain ⟨hsym, htr, htrans, hfrob⟩ := h
 208  constructor
 209  · intro hcE
 210    have hpin := hcE.2.2.2
 211    have hfrob' : frobeniusSq (c • E) = 1 := hpin
 212    rw [frobeniusSq_smul] at hfrob'
 213    have hfrobE : frobeniusSq E = 1 := hfrob
 214    rw [hfrobE, mul_one] at hfrob'
 215    exact hfrob'
 216  · intro hc2
 217    refine ⟨?_, ?_, ?_, ?_⟩
 218    · intro i j
 219      show c * E i j = c * E j i
 220      rw [hsym i j]
 221    · show (∑ i : Fin 3, c * E i i) = 0
 222      rw [← Finset.mul_sum, htr, mul_zero]
 223    · intro j
 224      show (∑ i : Fin 3, (m i : ℝ) * (c * E i j)) = 0
 225      calc (∑ i : Fin 3, (m i : ℝ) * (c * E i j))
 226          = c * ∑ i : Fin 3, (m i : ℝ) * E i j := by
 227            rw [Finset.mul_sum]
 228            exact Finset.sum_congr rfl fun i _ => by ring
 229        _ = 0 := by rw [htrans j, mul_zero]
 230    · have h1 : frobeniusSq (c • E) = c ^ 2 * frobeniusSq E :=
 231        frobeniusSq_smul c E
 232      have h2 : frobeniusSq E = 1 := hfrob
 233      show frobeniusSq (c • E) = 1
 234      rw [h1, h2, hc2, mul_one]
 235
 236/-- **GATE A0 VERDICT (THEOREM): the `-1/4` target statement is
 237well-posed under the `polEdgeCoeff` scaling convention.**
 238
 239The three clauses, all kernel-checked, assemble the well-posedness
 240argument:
 241
 2421. (pin) every `E` in the target's hypothesis class `IsTTPolarization`
 243   has Frobenius square-sum exactly `1`;
 2442. (quadratic scaling) the Bloch symbol value transforms as `H ↦ c²·H`
 245   under `E ↦ c·E`, so WITHOUT a normalization the fixed-value claim
 246   would be contradictory (the same family would report `H` and `c²·H`);
 2473. (pin bites) the only rescalings that stay inside the hypothesis class
 248   are `c² = 1`, and for those `c²·H = H` — the reported value is
 249   invariant on the quantified class.
 250
 251Hence `ReggeTTContinuumIsotropyTarget`, which quantifies over
 252`IsTTPolarization` (pin included), assigns a scaling-coherent meaning to
 253the fixed constant `reggeTTContinuumCoefficient = -(1/4)`.  Nothing here
 254proves (or evidences) that the value IS `-1/4`; that target remains OPEN
 255with status flag `false`. -/
 256theorem reggeTT_target_scaling_wellPosed {c : ℝ} (hc : c ≠ 0)
 257    (m : Fin 3 → ℤ) (E : Fin 3 → Fin 3 → ℝ) (H : ℝ)
 258    (hE : IsTTPolarization m E) :
 259    frobeniusSq E = 1 ∧
 260      (TTBlochSymbolIs N E m H ↔ TTBlochSymbolIs N (c • E) m (c ^ 2 * H)) ∧
 261      (IsTTPolarization m (c • E) ↔ c ^ 2 = 1) :=
 262  ⟨isTTPolarization_frobenius_pinned m E hE,
 263    TTBlochSymbolIs_smul N hc E m H,
 264    isTTPolarization_smul_iff m E c hE⟩
 265
 266end
 267
 268end ReggeTTSymbolSpecificationAudit
 269end Analysis
 270end Gravity
 271end IndisputableMonolith
 272