IndisputableMonolith.Gravity.SevenGaps.FreudenthalTorusClassMass

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.PathSumProbes
   3import IndisputableMonolith.Gravity.SevenGaps.ClassPushforward
   4
   5/-!
   6# Seven Gaps, Crux-2 consistency gate: torus class mass, labeled vs class
   7
   8## Protocol: QUOTIENT_BOOKKEEPING (panel-locked).
   9
  10## WORDING REPAIR (recorded per the panel's C6 trap)
  11
  12The originally-worded gate ("the class summand of the canonical torus in
  13the pushforward form is suppressed as N⁻³") is ILL-POSED as stated,
  14because the pushforward class mass is `|fiber| · (1/|Aut|)`
  15(`PathSum.classMass_eq_fiberCard_mul_mu`) and the labeled fiber
  16cardinality GROWS with the class size.  The panel's own kill list forbids
  17the absolute N⁻³ / N⁻⁶ suppression claim for the PUSHFORWARD mass.  This
  18module implements the honest split, keeping the two objects separated in
  19the type system:
  20
  21**THEOREM (proved below, 0 sorry, 0 new axioms) — the LABELED object:**
  22* `mu_torusClassMember_le`: EVERY labeled member `K` of the torus class
  23  (`⟦K⟧ = ⟦T_N⟧`) has symmetry-factor mass `μ(K) ≤ 1/N³` (the per-`1/|Aut|`
  24  statement, derived from `mu_congr` + `mu_freudenthal_le_inv_cube`).
  25* `norm_freudenthal_labeledSummand_le`: the single-labeled-representative
  26  summand `‖μ(K) · z‖ ≤ 1/N³` for any unit-modulus `z` and any labeled
  27  member `K` of the torus class (the class-API restatement of
  28  `unnormalized_torus_weight_suppressed`).
  29* `tendsto_mu_freudenthal_zero` and `tendsto_labeledSummand_zero`: the
  30  labeled-representative summand sequence
  31  `fun N => μ(T_{N+1}) · z_N` (any unit-modulus `z_N`) tends to `0`.
  32
  33**THEOREM — the CLASS object (with the honest fiber factor):**
  34* `torus_classMass_eq_fiberCard_mul_mu`: the pushforward class mass of the
  35  torus class equals `|fiber| · μ(T_N)`.
  36* `torus_classMass_le_fiberCard_div_cube`:
  37  `classMass(⟦T_N⟧) ≤ |fiber| / N³`.  The fiber cardinality is NOT
  38  bounded here (it grows with the labeled class), so this does NOT give
  39  an absolute N⁻³ suppression of the pushforward mass.
  40
  41**FORBIDDEN (not claimed anywhere in this module):**
  42* "classMass(⟦T_N⟧) ≤ 1/N³" — FALSE in general; the killed absolute
  43  pushforward-suppression claim.  Reason: `|fiber|` grows.
  44* Any convergence / continuum-limit / dominance claim about `Z`.
  45
  46**OPEN (flags stay RED; nothing here changes them):**
  47* `Z_RS_continuum_limit` : RED.
  48* `substrate_measure_derived` : RED.
  49* `gap1_bridge_derived` : RED.
  50
  51## Proof notes
  52* Zero `sorry`, zero `admit`, zero new axioms, zero `decide` /
  53  `native_decide` in this module.
  54* The tendsto statements are about the LABELED representative sequence
  55  only, exactly as the honest gate requires.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Gravity
  60namespace SevenGaps
  61namespace FreudenthalTorusClassMass
  62
  63open PathSumMeasure
  64open PathSumProbes
  65open PathSum
  66open FiniteQuotient
  67
  68/-! ## §1. The LABELED object: per-representative `1/|Aut|` suppression -/
  69
  70/-- **THEOREM (labeled, per-`1/|Aut|`).**  Every labeled member of the
  71torus class carries symmetry-factor mass at most `N⁻³`: μ is a class
  72function (`mu_congr`), and the translation embedding gives
  73`μ(T_N) ≤ 1/N³`.  This is a statement about EACH labeled representative,
  74not about the pushforward class mass. -/
  75theorem mu_torusClassMember_le (N : ℕ) [NeZero N]
  76    (K : BoundedComplex (7 * N ^ 3))
  77    (hK : Quotient.mk (relabelSetoid (7 * N ^ 3)) K =
  78      Quotient.mk (relabelSetoid (7 * N ^ 3)) (freudenthalBoundedComplex N)) :
  79    mu K ≤ 1 / ((N : ℝ) ^ 3) := by
  80  rw [mu_congr (equivalent_of_mk_eq hK)]
  81  exact mu_freudenthal_le_inv_cube N
  82
  83/-- **THEOREM (labeled summand bound; class-API restatement of
  84`unnormalized_torus_weight_suppressed`).**  For any labeled member `K` of
  85the torus class and any unit-modulus value `z`, the single labeled
  86summand `μ(K)·z` has modulus at most `N⁻³`.  LABELED / CLASS DISTINCTION:
  87this bounds ONE labeled summand; the pushforward CLASS mass is
  88`|fiber|·μ` and is NOT bounded by `N⁻³` here. -/
  89theorem norm_freudenthal_labeledSummand_le (N : ℕ) [NeZero N]
  90    (K : BoundedComplex (7 * N ^ 3))
  91    (hK : Quotient.mk (relabelSetoid (7 * N ^ 3)) K =
  92      Quotient.mk (relabelSetoid (7 * N ^ 3)) (freudenthalBoundedComplex N))
  93    (z : ℂ) (hz : ‖z‖ ≤ 1) :
  94    ‖(mu K : ℂ) * z‖ ≤ 1 / ((N : ℝ) ^ 3) := by
  95  rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos K)]
  96  calc mu K * ‖z‖
  97      ≤ mu K * 1 := mul_le_mul_of_nonneg_left hz (le_of_lt (mu_pos K))
  98    _ = mu K := mul_one _
  99    _ ≤ 1 / ((N : ℝ) ^ 3) := mu_torusClassMember_le N K hK
 100
 101/-! ## §2. The CLASS object: the honest fiber factor -/
 102
 103/-- **THEOREM (class mass, identity form).**  The pushforward class mass
 104of the torus class is the labeled fiber cardinality times the symmetry
 105factor of the canonical torus:
 106`classMass(⟦T_N⟧) = |fiber(⟦T_N⟧)| · μ(T_N)`. -/
 107theorem torus_classMass_eq_fiberCard_mul_mu (N : ℕ) [NeZero N] :
 108    classMass (Quotient.mk (relabelSetoid (7 * N ^ 3))
 109        (freudenthalBoundedComplex N)) =
 110      (fiberCard (relabelSetoid (7 * N ^ 3))
 111          (Quotient.mk (relabelSetoid (7 * N ^ 3))
 112            (freudenthalBoundedComplex N)) : ℝ) *
 113        mu (freudenthalBoundedComplex N) := by
 114  rw [classMass_eq_fiberCard_mul_mu]
 115  congr 1
 116  exact mu_congr (equivalent_of_mk_eq (Quotient.out_eq _))
 117
 118/-- **THEOREM (the honest class-mass bound).**
 119`classMass(⟦T_N⟧) ≤ |fiber(⟦T_N⟧)| / N³`.  The fiber cardinality is NOT
 120bounded here; in particular this does NOT yield the (killed) absolute
 121`N⁻³` suppression of the pushforward mass. -/
 122theorem torus_classMass_le_fiberCard_div_cube (N : ℕ) [NeZero N] :
 123    classMass (Quotient.mk (relabelSetoid (7 * N ^ 3))
 124        (freudenthalBoundedComplex N)) ≤
 125      (fiberCard (relabelSetoid (7 * N ^ 3))
 126          (Quotient.mk (relabelSetoid (7 * N ^ 3))
 127            (freudenthalBoundedComplex N)) : ℝ) / ((N : ℝ) ^ 3) := by
 128  rw [torus_classMass_eq_fiberCard_mul_mu, div_eq_mul_one_div]
 129  exact mul_le_mul_of_nonneg_left (mu_freudenthal_le_inv_cube N)
 130    (Nat.cast_nonneg _)
 131
 132/-! ## §3. Tendsto-zero for the LABELED representative sequence -/
 133
 134/-- The dominating sequence `1/(n+1)³` is below `1/(n+1)`. -/
 135theorem one_div_cube_le_one_div (n : ℕ) :
 136    1 / (((n : ℝ) + 1) ^ 3) ≤ 1 / ((n : ℝ) + 1) := by
 137  have h1 : (1 : ℝ) ≤ (n : ℝ) + 1 := le_add_of_nonneg_left (Nat.cast_nonneg n)
 138  have hpos : (0 : ℝ) < (n : ℝ) + 1 := lt_of_lt_of_le one_pos h1
 139  exact one_div_le_one_div_of_le hpos (le_self_pow₀ h1 (by norm_num))
 140
 141/-- **THEOREM (labeled tendsto, measure form).**  The symmetry-factor mass
 142of the canonical torus LABELED representative tends to zero:
 143`μ(T_{N+1}) → 0`.  (Squeeze between `0` and `1/(N+1)³ ≤ 1/(N+1)`.) -/
 144theorem tendsto_mu_freudenthal_zero :
 145    Filter.Tendsto (fun n : ℕ => mu (freudenthalBoundedComplex (n + 1)))
 146      Filter.atTop (nhds 0) := by
 147  refine squeeze_zero (fun n => le_of_lt (mu_pos _)) (fun n => ?_)
 148    tendsto_one_div_add_atTop_nhds_zero_nat
 149  calc mu (freudenthalBoundedComplex (n + 1))
 150      ≤ 1 / (((n + 1 : ℕ) : ℝ) ^ 3) := mu_freudenthal_le_inv_cube (n + 1)
 151    _ = 1 / (((n : ℝ) + 1) ^ 3) := by rw [Nat.cast_add, Nat.cast_one]
 152    _ ≤ 1 / ((n : ℝ) + 1) := one_div_cube_le_one_div n
 153
 154/-- **THEOREM (labeled tendsto, summand form; the honest T4 gate).**  The
 155labeled-representative summand sequence `μ(T_{N+1}) · z_N`, for ANY
 156sequence of unit-modulus values (e.g. `unitaryWeight` values of any
 157action), tends to `0`.  LABELED / CLASS DISTINCTION: this is the labeled
 158representative sequence; NO claim is made about the pushforward CLASS
 159mass sequence `|fiber|·μ`, whose fiber factor grows. -/
 160theorem tendsto_labeledSummand_zero (z : ℕ → ℂ) (hz : ∀ n, ‖z n‖ ≤ 1) :
 161    Filter.Tendsto
 162      (fun n : ℕ => (mu (freudenthalBoundedComplex (n + 1)) : ℂ) * z n)
 163      Filter.atTop (nhds 0) := by
 164  rw [tendsto_zero_iff_norm_tendsto_zero]
 165  refine squeeze_zero (fun n => norm_nonneg _) (fun n => ?_)
 166    tendsto_mu_freudenthal_zero
 167  rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos _)]
 168  exact mul_le_of_le_one_right (le_of_lt (mu_pos _)) (hz n)
 169
 170/-! ## §4. Status ledger (rfl-forced; RED flags stay RED) -/
 171
 172/-- Status record for the torus class-mass consistency gate.  No `True`
 173shells; every flag is forced by `rfl` below. -/
 174structure TorusClassMassStatus where
 175  labeled_member_mass_bounded : Bool
 176  labeled_summand_bounded : Bool
 177  labeled_summand_tendsto_zero : Bool
 178  classMass_identity_proved : Bool
 179  classMass_fiberCard_bound_proved : Bool
 180  /-- FALSE (killed claim, wording repair recorded in the header): the
 181  pushforward class mass is NOT absolutely `N⁻³`-suppressed; the labeled
 182  fiber cardinality grows. -/
 183  pushforward_classMass_absolutely_suppressed : Bool
 184  /-- RED. -/
 185  Z_RS_continuum_limit : Bool
 186  /-- RED. -/
 187  substrate_measure_derived : Bool
 188  /-- RED. -/
 189  gap1_bridge_derived : Bool
 190
 191/-- The consistency-gate status after this module. -/
 192def torusClassMassStatus : TorusClassMassStatus where
 193  labeled_member_mass_bounded := true
 194  labeled_summand_bounded := true
 195  labeled_summand_tendsto_zero := true
 196  classMass_identity_proved := true
 197  classMass_fiberCard_bound_proved := true
 198  pushforward_classMass_absolutely_suppressed := false
 199  Z_RS_continuum_limit := false
 200  substrate_measure_derived := false
 201  gap1_bridge_derived := false
 202
 203theorem torusClassMassStatus_flags :
 204    torusClassMassStatus.labeled_member_mass_bounded = true ∧
 205    torusClassMassStatus.labeled_summand_bounded = true ∧
 206    torusClassMassStatus.labeled_summand_tendsto_zero = true ∧
 207    torusClassMassStatus.classMass_identity_proved = true ∧
 208    torusClassMassStatus.classMass_fiberCard_bound_proved = true ∧
 209    torusClassMassStatus.pushforward_classMass_absolutely_suppressed = false ∧
 210    torusClassMassStatus.Z_RS_continuum_limit = false ∧
 211    torusClassMassStatus.substrate_measure_derived = false ∧
 212    torusClassMassStatus.gap1_bridge_derived = false :=
 213  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
 214
 215end FreudenthalTorusClassMass
 216end SevenGaps
 217end Gravity
 218end IndisputableMonolith
 219