IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit
   2
   3/-!
   4# Regge TT bucket-fiber aggregation (Gate C-A2f)
   5
   6QG full-theory campaign, Paper C / Pillar 1, Lane C of the finishing
   7charter.  This module closes the bucket-fiber aggregation gate left OPEN by
   8`ReggeTTBlochInterfaceAudit`: the radical-bearing raw stencil coefficient
   9`J_fg / (2 * sqrt a*_f)` (with `J = flatAngleJacobian` the flat angle
  10Jacobian and `a* = freudenthalTetSqEdges` the flat tuple) equals a literal
  11rational table on EVERY bucket, all 36 slot pairs, not just the row-0 smoke
  12bucket and the worst radical entry already kernel-recorded there.
  13
  14## Anti-tautology structure (binding)
  15
  16* `rationalStencilWeight` below is an INDEPENDENT literal table: a bare
  17  36-branch match on the bucket's slot pair with literal rational values.
  18  It is NOT defined as any fiber sum, radical expression, or alias of
  19  `rawJacobianCoefficient`; the two sides of the headline are independently
  20  defined objects.
  21* The headline `aggregate_raw_weight_eq_rational` proves, for EVERY bucket
  22  `b` (all slot pairs, all integer phase keys), that the actual
  23  radical-bearing coefficient `rawJacobianCoefficient b.left b.right`
  24  (defined in the interface audit from `flatAngleJacobian` and
  25  `freudenthalTetSqEdges`, both of which come from the kernel-proved A2/A3
  26  derivative machinery) equals the real cast of the table entry.
  27* The proof route is the proved Schlaefli radical bridge
  28  (`schlaefli_summand_bridge_edge0..5`, packaged as
  29  `schlaefliSummandBridge`): `sqrt(a*_f) * (dtheta_f/da_g) =
  30  (1/sqrt(2*cm3)) * schlaefliPolySummandNorm`, with `sqrt(2*cm3) = 4` at
  31  the flat tuple, so every entry is a RADICAL-FREE rational cofactor
  32  expression divided by `8 * a*_f`.  Each of the 36 entries is then closed
  33  by kernel rational arithmetic.  No numerics, no `native_decide`.
  34
  35## Value set
  36
  37The proved table takes values in `{0, 1/12, +-1/8, +-1/4}`.  The panel
  38preregistration expected `{0, +-1/4, -1/8}`; the kernel value set is the
  39strictly larger list above (row 1 diagonal carries `+1/8`, row 2 diagonal
  40carries `+1/12`, row 4 diagonal carries `+1/8`).  The two entries the
  41interface audit already recorded (`(0,5) = 1/4` smoke, `(1,2) = -1/8`
  42worst radical) are reproduced exactly, as corollaries of the headline.
  43
  44## Inherited axiom footprint (disclosure)
  45
  46Everything here is pure algebra over the derivative-gate chain; the
  47expected footprint of every theorem in this file is the standard trio
  48`[propext, Classical.choice, Quot.sound]`.  `#print axioms` receipts are
  49emitted at the end of the file.
  50
  51No `sorry`, no `admit`, no new axioms, no `native_decide`, no `: True` or
  52`Nonempty`-only headline in this file.
  53-/
  54
  55namespace IndisputableMonolith
  56namespace Gravity
  57namespace Analysis
  58namespace ReggeTTBucketAggregation
  59
  60open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges freudenthalTet)
  61open ReggeTTBlochInterfaceAudit (Bucket rawJacobianCoefficient row0SmokeBucket
  62  worstRadicalBucket)
  63
  64noncomputable section
  65
  66/-! ## §1. The independent literal rational table -/
  67
  68/-- THE FULL LITERAL RATIONAL TABLE (all 36 slot pairs).  This is an
  69independent literal table in the sense demanded by the panel: a bare match
  70with literal rational values, phase-independent, never defined through any
  71fiber sum or through `rawJacobianCoefficient`.  Derived offline from the
  72closed forms of `flatAngleJacobian` and `freudenthalTetSqEdges` and then
  73kernel-verified entry by entry in `aggregate_raw_weight_eq_rational`. -/
  74def rationalStencilWeight (b : Bucket) : ℚ :=
  75  match b.left, b.right with
  76  | 0, 0 => 0        | 0, 1 => 0        | 0, 2 => 0
  77  | 0, 3 => 0        | 0, 4 => -(1 / 8) | 0, 5 => 1 / 4
  78  | 1, 0 => 0        | 1, 1 => 1 / 8    | 1, 2 => -(1 / 8)
  79  | 1, 3 => -(1 / 4) | 1, 4 => 1 / 4    | 1, 5 => -(1 / 8)
  80  | 2, 0 => 0        | 2, 1 => -(1 / 8) | 2, 2 => 1 / 12
  81  | 2, 3 => 1 / 4    | 2, 4 => -(1 / 8) | 2, 5 => 0
  82  | 3, 0 => 0        | 3, 1 => -(1 / 4) | 3, 2 => 1 / 4
  83  | 3, 3 => 1 / 4    | 3, 4 => -(1 / 4) | 3, 5 => 0
  84  | 4, 0 => -(1 / 8) | 4, 1 => 1 / 4    | 4, 2 => -(1 / 8)
  85  | 4, 3 => -(1 / 4) | 4, 4 => 1 / 8    | 4, 5 => 0
  86  | 5, 0 => 1 / 4    | 5, 1 => -(1 / 8) | 5, 2 => 0
  87  | 5, 3 => 0        | 5, 4 => 0        | 5, 5 => 0
  88
  89/-! ## §2. The radical-free normal form of every raw coefficient -/
  90
  91/-- Every raw coefficient is the rationalized Schlaefli summand divided by
  92`8 * a*_f`: `J_fg / (2 * sqrt a*_f) = schlaefliPolySummandNorm(a*, f, g) /
  93(8 * a*_f)`.  Route: the proved radical bridge
  94`sqrt(a_f) * (dtheta_f/da_g) = (1/sqrt(2*cm3)) * norm` with
  95`sqrt(2 * cm3 a*) = sqrt 16 = 4` at the flat tuple, then
  96`sqrt(a_f) * sqrt(a_f) = a_f`.  No radical survives on the right. -/
  97theorem rawJacobianCoefficient_eq_norm_div (f g : Fin 6) :
  98    rawJacobianCoefficient f g =
  99      Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
 100          freudenthalTetSqEdges f g /
 101        (8 * freudenthalTetSqEdges f) := by
 102  have hb := Geometry.SchlaefliTetrahedronProof.schlaefliSummandBridge
 103    freudenthalTet f g
 104  have h4 : Real.sqrt (2 * Geometry.CayleyMengerPolynomial.cm3
 105      freudenthalTet.sqEdge) = 4 := by
 106    have hcm : Geometry.CayleyMengerPolynomial.cm3 freudenthalTet.sqEdge = 8 :=
 107      Geometry.FreudenthalCubeTriangulation.cm3_freudenthalTetSqEdges
 108    rw [hcm, show (2 : ℝ) * 8 = 4 ^ 2 by norm_num,
 109      Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 4)]
 110  rw [h4] at hb
 111  have hJ : ReggeTTDerivativeGate.flatAngleJacobian f g =
 112      Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
 113        freudenthalTet f g := by
 114    rw [ReggeTTDerivativeGate.flatAngleJacobian_eq_dihedralClosedDerivSq]
 115    exact Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSq_eq_poly
 116      freudenthalTet f g
 117  have hpos : (0 : ℝ) < freudenthalTetSqEdges f := freudenthalTet.sqEdge_pos f
 118  have hsqrt_ne : Real.sqrt (freudenthalTetSqEdges f) ≠ 0 :=
 119    ne_of_gt (Real.sqrt_pos.mpr hpos)
 120  have hsq : Real.sqrt (freudenthalTetSqEdges f) *
 121      Real.sqrt (freudenthalTetSqEdges f) = freudenthalTetSqEdges f :=
 122    Real.mul_self_sqrt hpos.le
 123  unfold rawJacobianCoefficient
 124  rw [hJ]
 125  rw [show freudenthalTet.sqEdge = freudenthalTetSqEdges from rfl] at hb
 126  rw [div_eq_div_iff
 127    (by positivity : (2 : ℝ) * Real.sqrt (freudenthalTetSqEdges f) ≠ 0)
 128    (by positivity : (8 : ℝ) * freudenthalTetSqEdges f ≠ 0)]
 129  calc
 130    Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
 131          freudenthalTet f g * (8 * freudenthalTetSqEdges f)
 132        = 8 * (Real.sqrt (freudenthalTetSqEdges f) *
 133            Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
 134              freudenthalTet f g) * Real.sqrt (freudenthalTetSqEdges f) := by
 135          rw [show Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
 136                freudenthalTet f g * (8 * freudenthalTetSqEdges f) =
 137              8 * (Geometry.SchlaefliTetrahedronProof.dihedralClosedDerivSqPoly
 138                freudenthalTet f g *
 139                (Real.sqrt (freudenthalTetSqEdges f) *
 140                  Real.sqrt (freudenthalTetSqEdges f))) by rw [hsq]; ring]
 141          ring
 142    _ = 8 * (1 / 4 *
 143          Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
 144            freudenthalTetSqEdges f g) * Real.sqrt (freudenthalTetSqEdges f) := by
 145          rw [hb]
 146    _ = Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm
 147          freudenthalTetSqEdges f g *
 148            (2 * Real.sqrt (freudenthalTetSqEdges f)) := by
 149          ring
 150
 151/-- All 36 raw coefficients evaluated to exact rationals.  Each entry is
 152the radical-free normal form of `rawJacobianCoefficient_eq_norm_div`
 153evaluated by kernel rational arithmetic on the flat integer tuple. -/
 154theorem rawJacobianCoefficient_eval (f g : Fin 6) :
 155    rawJacobianCoefficient f g =
 156      ((rationalStencilWeight ⟨f, g, fun _ => 0⟩ : ℚ) : ℝ) := by
 157  rw [rawJacobianCoefficient_eq_norm_div]
 158  fin_cases f <;> fin_cases g <;>
 159    norm_num [rationalStencilWeight,
 160      Geometry.SchlaefliTetrahedronProof.schlaefliPolySummandNorm,
 161      Geometry.CofactorPolynomial.cmCofactor3Poly,
 162      Geometry.CofactorPolynomial.cmCofactorPartial,
 163      freudenthalTetSqEdges]
 164
 165/-! ## §3. The headline: fiber value = literal table on EVERY bucket -/
 166
 167/-- **GATE C-A2f HEADLINE (THEOREM): on EVERY bucket (every slot pair,
 168every integer phase key), the actual radical-bearing raw stencil
 169coefficient `J_{fg} / (2 * sqrt a*_f)` equals the real cast of the
 170independent literal rational table.**  The left side is
 171`rawJacobianCoefficient` of the interface audit (built from the
 172kernel-proved flat angle Jacobian and the flat tuple); the right side is
 173the bare literal table of §1.  The two sides are independently defined;
 174their equality is 36 kernel-checked radical cancellations. -/
 175theorem aggregate_raw_weight_eq_rational (b : Bucket) :
 176    rawJacobianCoefficient b.left b.right =
 177      ((rationalStencilWeight b : ℚ) : ℝ) := by
 178  have h := rawJacobianCoefficient_eval b.left b.right
 179  have htbl : rationalStencilWeight ⟨b.left, b.right, fun _ => 0⟩ =
 180      rationalStencilWeight b := rfl
 181  rw [htbl] at h
 182  exact h
 183
 184/-- The literal table is invariant under the bucket reversal
 185`(f, g, u) ~ (g, f, -u)`: the underlying 6x6 rational matrix is symmetric,
 186so the intended external quotient is well-defined on table values. -/
 187theorem rationalStencilWeight_swap (b : Bucket) :
 188    rationalStencilWeight b.swap = rationalStencilWeight b := by
 189  rcases b with ⟨l, r, u⟩
 190  fin_cases l <;> fin_cases r <;> rfl
 191
 192/-! ## §4. Consistency corollaries against the kernel-recorded audit facts -/
 193
 194/-- The table reproduces the interface audit's row-0 smoke value
 195(`rawJacobianCoefficient (0,5) = 1/4`, kernel-recorded there). -/
 196theorem table_matches_row0Smoke :
 197    ((rationalStencilWeight row0SmokeBucket : ℚ) : ℝ) =
 198      rawJacobianCoefficient ⟨0, by decide⟩ ⟨5, by decide⟩ :=
 199  (aggregate_raw_weight_eq_rational row0SmokeBucket).symm
 200
 201/-- The table reproduces the interface audit's worst-radical value
 202(`rawJacobianCoefficient (1,2) = -1/8`, kernel-recorded there through the
 203`-sqrt 2 / 4` Jacobian entry). -/
 204theorem table_matches_worstRadical :
 205    ((rationalStencilWeight worstRadicalBucket : ℚ) : ℝ) = -(1 / 8 : ℝ) := by
 206  rw [← aggregate_raw_weight_eq_rational worstRadicalBucket]
 207  exact ReggeTTBlochInterfaceAudit.worstRadical_rawJacobianCoefficient_closedForm
 208
 209end
 210
 211end ReggeTTBucketAggregation
 212end Analysis
 213end Gravity
 214end IndisputableMonolith
 215
 216#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.rawJacobianCoefficient_eq_norm_div
 217#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.rawJacobianCoefficient_eval
 218#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.aggregate_raw_weight_eq_rational
 219#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.rationalStencilWeight_swap
 220#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.table_matches_row0Smoke
 221#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTBucketAggregation.table_matches_worstRadical
 222