IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTFlatSecondVariation
   2
   3/-!
   4# Regge TT Bloch interface audit, attempt 2
   5
   6This is the panel-locked C11 interface audit surface.  Attempt 1 was rejected
   7because it wired the raw stencil and rational bucket table definitionally to
   8the objects they were supposed to audit.  This file therefore keeps the first
   9gate deliberately narrow and non-tautological:
  10
  11* `rawCellStencil` is a literal `6 x 6 x 6`-shape triple sum over tetrahedra
  12  and ordered slot pairs.  The inner `g` sum of `flatSlotAngleDeriv` is
  13  expanded here, and `flatSlotSqrtDeriv` is written as
  14  `planeWaveTetVelocity / (2 * sqrt a*)`.
  15* `a2_reduced_eq_rawCellStencil` proves the A2 reduced value equals that
  16  triple sum by distributing the finite inner sum.  The sign follows the live
  17  A2 theorem: the reduced second variation is the negative Schlaefli-reduced
  18  contraction.
  19* The full rational bucket aggregation and assembled zero-mode cancellation
  20  are not claimed here.  The same-day sympy diagnostic found that the
  21  stencil-only constant block does not vanish; the ContinuumLimit engine must
  22  use the cosine two-jet route after the hinge/diagonal constant block is
  23  formally connected.
  24
  25Status block:
  26
  27* Gate A2-full (`aggregate_raw_weight_eq_rational` over all buckets): OPEN.
  28* Gate A3 (hinge-aware zero-mode): OPEN.
  29* Gate B (spike convention bridge): OPEN; the sidecar states
  30  `GateBConventionTarget`.
  31
  32No ContinuumLimit or spike certificate module is imported here.
  33-/
  34
  35namespace IndisputableMonolith
  36namespace Gravity
  37namespace Analysis
  38namespace ReggeTTBlochInterfaceAudit
  39
  40open Geometry.PeriodicFreudenthalTorus
  41open Geometry.FreudenthalCubeTriangulation (freudenthalTetSqEdges)
  42open ReggeTTSymbolPreflight
  43open ReggeTTFlatSecondVariation
  44
  45noncomputable section
  46
  47/-- One raw term of the cell stencil: tetrahedron type and ordered slot pair.
  48The concrete finite sum below has `6 x 6 x 6 = 216` summands per periodic cell
  49type. -/
  50structure RawCellStencilTerm where
  51  tet : Fin 6
  52  left : Fin 6
  53  right : Fin 6
  54deriving DecidableEq, Repr
  55
  56/-- Integer displacement key for phase buckets. -/
  57abbrev PhaseVector := Fin 3 → Int
  58
  59/-- Bucket representative.  The intended external convention only identifies
  60`(f,g,u)` with `(g,f,-u)`; this attempt does not yet quotient or aggregate all
  61fibers. -/
  62structure Bucket where
  63  left : Fin 6
  64  right : Fin 6
  65  phase : PhaseVector
  66deriving DecidableEq, Repr
  67
  68/-- Negate a phase key. -/
  69def negPhase (u : PhaseVector) : PhaseVector := fun i => -u i
  70
  71/-- The reversal representative associated to `(f,g,u) ~ (g,f,-u)`. -/
  72def Bucket.swap (b : Bucket) : Bucket :=
  73  ⟨b.right, b.left, negPhase b.phase⟩
  74
  75/-- Literal rational table placeholder for the bucket quarantine.  It is an
  76independent table, not a fiber sum.  Only the row-0 smoke bucket is proved
  77against actual Jacobian data in this attempt. -/
  78def rationalStencilWeight (b : Bucket) : ℚ :=
  79  match b.left, b.right with
  80  | ⟨0, _⟩, ⟨5, _⟩ => 1 / 4
  81  | ⟨5, _⟩, ⟨0, _⟩ => 1 / 4
  82  | _, _ => 0
  83
  84/-- The reduced A2 canonical finite value, named for the interface audit. -/
  85def canonicalFiniteH (N : ℕ) [NeZero N] (E : Fin 3 → Fin 3 → ℝ)
  86    (m : Fin 3 → ℤ) : ℝ :=
  87  (2 / (N : ℝ) ^ (3 : ℕ)) *
  88    (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
  89      flatSlotSqrtDeriv N E (commensurateMomentum N m) τ f *
  90        flatSlotAngleDeriv N E (commensurateMomentum N m) τ f)
  91
  92/-- The raw triple stencil term, with the `g`-sum exposed and the sqrt-edge
  93factor unfolded to `v_f / (2 * sqrt a*_f)`. -/
  94def rawCellStencilTerm (N : ℕ) [NeZero N] (E : Fin 3 → Fin 3 → ℝ)
  95    (m : Fin 3 → ℤ) (τ : PeriodicTet N N N) (f g : Fin 6) : ℝ :=
  96  (ReggeTTLocalSymbolExistence.planeWaveTetVelocity
  97      N E (commensurateMomentum N m) τ f /
  98      (2 * Real.sqrt (freudenthalTetSqEdges f))) *
  99    ReggeTTLocalSymbolExistence.planeWaveTetVelocity
 100      N E (commensurateMomentum N m) τ g *
 101      ReggeTTDerivativeGate.flatAngleJacobian f g
 102
 103/-- Raw cell-stencil expression as an explicit triple sum. -/
 104def rawCellStencil (N : ℕ) [NeZero N] (E : Fin 3 → Fin 3 → ℝ)
 105    (m : Fin 3 → ℤ) : ℝ :=
 106  (2 / (N : ℝ) ^ (3 : ℕ)) *
 107    (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
 108      rawCellStencilTerm N E m τ f g)
 109
 110/-- Gate A1, honest part: the A2 reduced finite value equals the literal
 111triple raw stencil.  The proof is finite distribution of the inner
 112`flatSlotAngleDeriv` sum, not a definitional alias between the two sides.
 113The panel's `hN` premise is not needed: the incidence identity holds for
 114every `N` with `[NeZero N]`, which is a strictly stronger statement. -/
 115theorem a2_reduced_eq_rawCellStencil (N : ℕ) [NeZero N]
 116    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
 117    canonicalFiniteH N E m = rawCellStencil N E m := by
 118  unfold canonicalFiniteH rawCellStencil rawCellStencilTerm
 119  congr 1
 120  congr 1
 121  refine Finset.sum_congr rfl fun τ _ => ?_
 122  refine Finset.sum_congr rfl fun f _ => ?_
 123  unfold flatSlotSqrtDeriv flatSlotAngleDeriv
 124  rw [Finset.mul_sum]
 125  refine Finset.sum_congr rfl fun g _ => ?_
 126  ring_nf
 127
 128/-- Row-0 smoke-test bucket: `J_05 / (2 * sqrt a*_0)` with
 129`freudenthalTetSqEdges 0 = 1`, so this is radical-trivial. -/
 130def row0SmokeBucket : Bucket :=
 131  ⟨⟨0, by decide⟩, ⟨5, by decide⟩, fun _ => 0⟩
 132
 133/-- Actual single-entry radical coefficient used by the early bucket
 134falsifier.  This is not the full fiber aggregation. -/
 135def rawJacobianCoefficient (f g : Fin 6) : ℝ :=
 136  ReggeTTDerivativeGate.flatAngleJacobian f g /
 137    (2 * Real.sqrt (freudenthalTetSqEdges f))
 138
 139/-- Row-0 smoke test: the radical-trivial coefficient
 140`J_05 / (2 * sqrt a*_0)` is the literal rational `1/4`. -/
 141theorem row0Smoke_raw_weight_eq_rational :
 142    rawJacobianCoefficient ⟨0, by decide⟩ ⟨5, by decide⟩ = (1 / 4 : ℝ) := by
 143  unfold rawJacobianCoefficient
 144  change ReggeTTDerivativeGate.flatAngleJacobian (0 : Fin 6) ⟨5, by decide⟩ /
 145      (2 * Real.sqrt (freudenthalTetSqEdges (0 : Fin 6))) = (1 / 4 : ℝ)
 146  rw [ReggeTTDerivativeGate.flatAngleJacobian_row0_eval ⟨5, by decide⟩]
 147  norm_num [ReggeTTDerivativeGate.flatAngleJacobianRow0,
 148    freudenthalTetSqEdges, Real.sqrt_one]
 149
 150/-- The independent table agrees with the row-0 smoke rational after casting
 151to real.  This is intentionally only the isolated smoke-test bucket, not the
 152full `aggregate_raw_weight_eq_rational` gate. -/
 153theorem row0Smoke_table_value :
 154    ((rationalStencilWeight row0SmokeBucket : ℚ) : ℝ) = (1 / 4 : ℝ) := by
 155  norm_num [rationalStencilWeight, row0SmokeBucket]
 156
 157/-- Genuine radical-row bucket selected by the exact sympy generator:
 158`(f,g) = (1,2)`, where `freudenthalTetSqEdges 1 = 2` and the angle-Jacobian
 159entry is nonzero. -/
 160def worstRadicalBucket : Bucket :=
 161  ⟨⟨1, by decide⟩, ⟨2, by decide⟩, fun _ => 0⟩
 162
 163/-- Genuine radical-row audit: at the row-Jacobian layer, individual raw
 164coefficients ARE irrational here; the panel's rationality claim lives at
 165bucket-fiber-AGGREGATION level and remains OPEN.  For this selected entry the
 166Jacobian is `-sqrt 2 / 4`; the current `rawJacobianCoefficient` normalization
 167then exposes and cancels the same `sqrt 2` denominator. -/
 168theorem worstRadical_flatAngleJacobian_value :
 169    ReggeTTDerivativeGate.flatAngleJacobian (1 : Fin 6) (2 : Fin 6) =
 170      -(Real.sqrt 2) / 4 := by
 171  rw [ReggeTTDerivativeGate.flatAngleJacobian_cofactor_form]
 172  rw [Geometry.CofactorDerivatives.dihedralCos3SqClosedFormDeriv_eq_poly]
 173  norm_num [ReggeTTDerivativeGate.flatArccosFactor,
 174    Geometry.CofactorDerivatives.dihedralCos3SqPolyClosedFormDeriv,
 175    Geometry.CofactorDerivatives.dihedralDenom3PolyClosedDerivValue,
 176    Geometry.CofactorDerivatives.dihedralDenom3Poly,
 177    Geometry.CofactorPolynomial.cmCofactor3Poly,
 178    Geometry.CofactorPolynomial.cmCofactorPartial,
 179    Geometry.DihedralCayleyMenger.oppositeCMVertices,
 180    freudenthalTetSqEdges]
 181  rw [show Real.sqrt 32 = 4 * Real.sqrt 2 by
 182    rw [show (32 : ℝ) = 16 * 2 by norm_num]
 183    rw [Real.sqrt_mul (by norm_num : (0 : ℝ) ≤ 16),
 184      show Real.sqrt (16 : ℝ) = 4 by norm_num]]
 185  ring
 186
 187/-- Exact raw coefficient for the genuine radical-row entry.  The statement
 188keeps the radical-bearing numerator visible; Lean also proves the normalized
 189coefficient simplifies to `-1/8`. -/
 190theorem worstRadical_rawJacobianCoefficient_closedForm :
 191    rawJacobianCoefficient ⟨1, by decide⟩ ⟨2, by decide⟩ = -(1 / 8 : ℝ) := by
 192  unfold rawJacobianCoefficient
 193  change ReggeTTDerivativeGate.flatAngleJacobian (1 : Fin 6) (2 : Fin 6) /
 194      (2 * Real.sqrt (freudenthalTetSqEdges (1 : Fin 6))) = -(1 / 8 : ℝ)
 195  rw [worstRadical_flatAngleJacobian_value]
 196  norm_num [freudenthalTetSqEdges]
 197  have hsqrt2_ne : Real.sqrt 2 ≠ 0 := by positivity
 198  field_simp [hsqrt2_ne]
 199  norm_num
 200
 201/-- Generic Bloch fold over a supplied support and phase evaluator. -/
 202def reggeTTBlochFold (support : Finset Bucket) (phase : Bucket → ℝ)
 203    (amplitude : Bucket → ℝ) : ℝ :=
 204  support.sum fun b => phase b * amplitude b
 205
 206/-- Cosine-evaluated assembled symbol surface. -/
 207def reggeTTAssembledSymbol (support : Finset Bucket) (phase : Bucket → ℝ)
 208    (amplitude : Bucket → ℝ) : ℝ :=
 209  reggeTTBlochFold support phase amplitude
 210
 211/-- Moment evaluator surface.  The evaluator is the stencil fold at the
 212cosine two-jet value `-z^2/2`; the campaign's frozen `x(1/4)` normalization
 213is represented by the caller-supplied phase quadratic.  This file does not
 214identify that fold with the committed spike polynomial. -/
 215def reggeTTMoment (support : Finset Bucket) (phaseQuadratic : Bucket → ℝ)
 216    (amplitude : Bucket → ℝ) : ℝ :=
 217  reggeTTBlochFold support (fun b => -(phaseQuadratic b) / 2) amplitude
 218
 219/-- Concrete record of the diagnostic zero-mode obstruction.  The
 220stencil-only constant block has the displayed nonzero residual for the
 221reported TT witness; the hinge/diagonal O(1) term is the remaining formal
 222interface piece needed before a true zero-mode theorem can be stated. -/
 223def stencilOnlyConstantWitnessResidual : ℝ :=
 224  -Real.pi * (Real.sqrt 2 + 4) / 8
 225
 226end
 227
 228end ReggeTTBlochInterfaceAudit
 229end Analysis
 230end Gravity
 231end IndisputableMonolith
 232