IndisputableMonolith.Gravity.TensorShearSector

   1import Mathlib
   2import IndisputableMonolith.Geometry.ReggeActionFirstVariation
   3import IndisputableMonolith.Geometry.PeriodicFreudenthalTorus
   4
   5/-!
   6# Track 1.D tensor/shear sector scaffold
   7
   8The existing Track 1.B conformal ansatz assigns one scalar potential to each
   9vertex and induces edge-length variations by averaging endpoint potentials.
  10That scalar slice is not the full weak-field metric sector: it cannot represent
  11pure shear, hence cannot by itself cover transverse-traceless gravitational-wave
  12modes.
  13
  14This file starts the tensor/shear track by separating independent edge
  15perturbations from vertex-conformal perturbations and by proving the elementary
  16rectangle obstruction for the conformal ansatz.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Gravity
  21namespace TensorShearSector
  22
  23open Geometry.ReggeTriangulation3D
  24open Geometry.ReggeHessian3D
  25open Geometry.ReggeActionFirstVariation
  26open Geometry.Triangulation3DConsistency
  27open Geometry.PeriodicFreudenthalTorus
  28
  29noncomputable section
  30
  31/-- Edge-level length perturbations.  Unlike `VertexPotential`, this has one
  32degree of freedom per global edge and is the natural finite Regge surface for
  33anisotropic shear and TT modes. -/
  34abbrev EdgePerturbation (K : Triangulation3D) :=
  35  Fin K.nE → ℝ
  36
  37/-- The first-order log-length strain induced by the vertex-conformal ansatz. -/
  38def conformalEdgeLogStrain (K : Triangulation3D) (ξ : VertexPotential K) :
  39    EdgePerturbation K :=
  40  fun e =>
  41    let uv := K.edgeVerts e
  42    (ξ uv.1 + ξ uv.2) / 2
  43
  44/-- The actual first-order length variation induced by the conformal ansatz. -/
  45def conformalEdgeLengthPerturbation
  46    (K : Triangulation3D) (hK : IncidenceConsistent K) (ξ : VertexPotential K) :
  47    EdgePerturbation K :=
  48  fun e => hingeMeasureDirectionalDeriv K hK ξ e
  49
  50theorem conformalEdgeLengthPerturbation_eq_sqrt_mul_logStrain
  51    (K : Triangulation3D) (hK : IncidenceConsistent K) (ξ : VertexPotential K)
  52    (e : Fin K.nE) :
  53    conformalEdgeLengthPerturbation K hK ξ e =
  54      Real.sqrt (hK.globalSqEdge e) * conformalEdgeLogStrain K ξ e := by
  55  rfl
  56
  57/-- The subspace of edge perturbations that come from vertex-conformal
  58potentials.  Track 1.B lives inside this subspace. -/
  59def IsConformalEdgePerturbation (K : Triangulation3D) (ε : EdgePerturbation K) : Prop :=
  60  ∃ ξ : VertexPotential K, ε = conformalEdgeLogStrain K ξ
  61
  62/-- Rectangle obstruction in first-order log strains.  If a quadrilateral's two
  63opposite horizontal edges have conformal log-strain `h` and its two opposite
  64vertical edges have conformal log-strain `v`, then `h = v`.  Hence a nontrivial
  65rectangle/shear mode cannot be vertex-conformal. -/
  66theorem vertexConformal_rectangle_log_strain_forces_square
  67    (ξa ξb ξc ξd h v : ℝ)
  68    (hab : (ξa + ξb) / 2 = h)
  69    (hcd : (ξc + ξd) / 2 = h)
  70    (hbc : (ξb + ξc) / 2 = v)
  71    (hda : (ξd + ξa) / 2 = v) :
  72    h = v := by
  73  linarith
  74
  75/-- A nontrivial rectangle/shear strain (`h ≠ v`) has no vertex-conformal
  76potential realization. -/
  77theorem nontrivial_rectangle_shear_not_vertexConformal
  78    (h v : ℝ) (hne : h ≠ v) :
  79    ¬ ∃ ξa ξb ξc ξd : ℝ,
  80      (ξa + ξb) / 2 = h ∧
  81      (ξc + ξd) / 2 = h ∧
  82      (ξb + ξc) / 2 = v ∧
  83      (ξd + ξa) / 2 = v := by
  84  rintro ⟨ξa, ξb, ξc, ξd, hab, hcd, hbc, hda⟩
  85  exact hne (vertexConformal_rectangle_log_strain_forces_square
  86    ξa ξb ξc ξd h v hab hcd hbc hda)
  87
  88/-! ## Concrete `N = 5` periodic Freudenthal edge surface -/
  89
  90abbrev PeriodicVertex5 :=
  91  Vertex 5 5 5
  92
  93abbrev PeriodicEdge5 :=
  94  PeriodicEdge 5 5 5
  95
  96/-- The canonical encoded `5 × 5 × 5` periodic Freudenthal torus for Track 1.D. -/
  97noncomputable abbrev PeriodicTorus5 :=
  98  canonicalEncodedPeriodicFreudenthalTorus 5 5 5 (by decide) (by decide) (by decide)
  99
 100/-- External vertex decoder matching the numerical order used by the Track 1.D
 101payload generators: `vertex_index = (x * 5 + y) * 5 + z`. -/
 102def periodicExternalVertexOfIndex5 (idx : Nat) : PeriodicVertex5 :=
 103  (⟨(idx / 25) % 5, by omega⟩,
 104   ⟨(idx / 5) % 5, by omega⟩,
 105   ⟨idx % 5, by omega⟩)
 106
 107/-- External vertex encoder matching `periodicExternalVertexOfIndex5` on
 108in-range payload vertices. -/
 109def periodicExternalVertexIndex5 (v : PeriodicVertex5) : Nat :=
 110  (v.1.1 * 5 + v.2.1.1) * 5 + v.2.2.1
 111
 112/-- External edge decoder matching the numerical order used by the Track 1.D
 113payload generators: `edge_index = vertex_index * 7 + disp`.  This is a
 114computable, Lean-native companion to the canonical `PeriodicTorus5.edgeEquiv`,
 115whose current implementation goes through opaque `Fintype.equivFin` order. -/
 116def periodicExternalEdgeOfEncodedIdx5
 117    (idx : Fin PeriodicTorus5.K.nE) : PeriodicEdge5 :=
 118  { base := periodicExternalVertexOfIndex5 (idx.1 / 7)
 119    disp := ⟨idx.1 % 7, by omega⟩ }
 120
 121/-- External edge encoder matching the numerical order used by the Track 1.D
 122payload generators. -/
 123def periodicExternalEdgeIndex5 (e : PeriodicEdge5) : Nat :=
 124  periodicExternalVertexIndex5 e.base * 7 + e.disp.1
 125
 126/-- Canonical encoded vertex index equivalence for the concrete `N = 5` torus. -/
 127noncomputable abbrev periodicVertexEquiv5 :
 128    Fin PeriodicTorus5.K.nV ≃ PeriodicVertex5 :=
 129  vertexFinEquiv 5 5 5
 130
 131/-- Coordinate addition on the concrete `N = 5` torus. -/
 132def periodicAddFin5 (base v : Fin 5) : Fin 5 :=
 133  ⟨(base.1 + v.1) % 5, by omega⟩
 134
 135/-- Translate a vertex by another vertex on the concrete `N = 5` torus. -/
 136def periodicTranslateVertex5 (base v : PeriodicVertex5) : PeriodicVertex5 :=
 137  (periodicAddFin5 base.1 v.1,
 138   periodicAddFin5 base.2.1 v.2.1,
 139   periodicAddFin5 base.2.2 v.2.2)
 140
 141/-- Encoded vertex-index shift corresponding to translation by a typed row base. -/
 142noncomputable def periodicTranslateEncodedVertexIdx5
 143    (base : PeriodicVertex5) (v : Fin PeriodicTorus5.K.nV) :
 144    Fin PeriodicTorus5.K.nV :=
 145  periodicVertexEquiv5.symm (periodicTranslateVertex5 base (periodicVertexEquiv5 v))
 146
 147/-- The encoded torus endpoint map agrees with the typed periodic-edge
 148endpoints after transporting through the canonical vertex equivalence. -/
 149theorem periodicTorus5_edgeVerts_symm_eq_endpoints
 150    (e : PeriodicEdge5) :
 151    PeriodicTorus5.K.edgeVerts (PeriodicTorus5.edgeEquiv.symm e) =
 152      (periodicVertexEquiv5.symm e.endpoints.1,
 153       periodicVertexEquiv5.symm e.endpoints.2) := by
 154  simp [periodicVertexEquiv5,
 155    canonicalEncodedPeriodicFreudenthalTorus,
 156    canonicalEncodedPeriodicFreudenthalTorus_of_endpoint,
 157    canonicalEncodedPeriodicFreudenthalTorus_of_incidence,
 158    canonicalPeriodicTriangulation, canonicalPeriodicEdgeEquiv,
 159    canonicalEdgeVerts]
 160
 161/-- Edge perturbations indexed by the typed periodic Freudenthal edges. -/
 162abbrev PeriodicEdgePerturbation5 :=
 163  PeriodicEdge5 → ℝ
 164
 165/-- Edge perturbations indexed by the encoded finite triangulation edges. -/
 166abbrev EncodedEdgePerturbation5 :=
 167  EdgePerturbation PeriodicTorus5.K
 168
 169/-- Pull an encoded finite edge perturbation back to typed periodic edges. -/
 170def encodedToPeriodicEdgePerturbation5
 171    (ε : EncodedEdgePerturbation5) : PeriodicEdgePerturbation5 :=
 172  fun e => ε (PeriodicTorus5.edgeEquiv.symm e)
 173
 174/-- Push a typed periodic edge perturbation to encoded finite edge indices. -/
 175def periodicToEncodedEdgePerturbation5
 176    (ε : PeriodicEdgePerturbation5) : EncodedEdgePerturbation5 :=
 177  fun e => ε (PeriodicTorus5.edgeEquiv e)
 178
 179/-- The encoded `Fin K.nE` and typed periodic-edge views of the `N = 5`
 180tensor/shear perturbation surface are exactly equivalent. -/
 181noncomputable def periodicEdgePerturbationEquiv5 :
 182    EncodedEdgePerturbation5 ≃ PeriodicEdgePerturbation5 where
 183  toFun := encodedToPeriodicEdgePerturbation5
 184  invFun := periodicToEncodedEdgePerturbation5
 185  left_inv := by
 186    intro ε
 187    funext e
 188    simp [encodedToPeriodicEdgePerturbation5, periodicToEncodedEdgePerturbation5]
 189  right_inv := by
 190    intro ε
 191    funext e
 192    simp [encodedToPeriodicEdgePerturbation5, periodicToEncodedEdgePerturbation5]
 193
 194/-- Raw additive splitting datum for an edge-perturbation space.  This carries
 195only the algebraic reconstruction identity; the real Track 1.D target below
 196adds conformal, gauge, and TT membership predicates. -/
 197structure RawEdgePerturbationSplitting (E : Type) where
 198  conformalPart : (E → ℝ) → E → ℝ
 199  gaugePart : (E → ℝ) → E → ℝ
 200  ttPart : (E → ℝ) → E → ℝ
 201  reconstruct :
 202    ∀ ε : E → ℝ, ∀ e : E,
 203      conformalPart ε e + gaugePart ε e + ttPart ε e = ε e
 204
 205/-- The concrete next target for Track 1.D after Session 215.  The three
 206predicates must be supplied by the actual periodic Freudenthal operators:
 207conformal/trace, gauge/longitudinal, and TT/transverse-traceless. -/
 208def PeriodicFreudenthalTTDecompositionTargetAtN5
 209    (IsConformal IsGauge IsTT : PeriodicEdgePerturbation5 → Prop) : Prop :=
 210  ∃ split : RawEdgePerturbationSplitting PeriodicEdge5,
 211    (∀ ε, IsConformal (split.conformalPart ε)) ∧
 212    (∀ ε, IsGauge (split.gaugePart ε)) ∧
 213    (∀ ε, IsTT (split.ttPart ε))
 214
 215/-- Carry any decomposition on encoded finite edges across the canonical
 216periodic-edge equivalence. -/
 217noncomputable def periodicRawSplittingOfEncoded5
 218    (D : RawEdgePerturbationSplitting (Fin PeriodicTorus5.K.nE)) :
 219    RawEdgePerturbationSplitting PeriodicEdge5 where
 220  conformalPart ε :=
 221    encodedToPeriodicEdgePerturbation5
 222      (D.conformalPart (periodicToEncodedEdgePerturbation5 ε))
 223  gaugePart ε :=
 224    encodedToPeriodicEdgePerturbation5
 225      (D.gaugePart (periodicToEncodedEdgePerturbation5 ε))
 226  ttPart ε :=
 227    encodedToPeriodicEdgePerturbation5
 228      (D.ttPart (periodicToEncodedEdgePerturbation5 ε))
 229  reconstruct := by
 230    intro ε e
 231    simp [encodedToPeriodicEdgePerturbation5, periodicToEncodedEdgePerturbation5,
 232      D.reconstruct]
 233
 234/-! ## Orthogonal conformal/gauge/TT surface -/
 235
 236/-- The finite `N = 5` edge-space inner product used for the tensor/shear
 237decomposition. -/
 238def periodicEdgeInnerProduct5
 239    (ε η : PeriodicEdgePerturbation5) : ℝ :=
 240  ∑ e : PeriodicEdge5, ε e * η e
 241
 242theorem periodicEdgeInnerProduct5_symm
 243    (ε η : PeriodicEdgePerturbation5) :
 244    periodicEdgeInnerProduct5 ε η = periodicEdgeInnerProduct5 η ε := by
 245  unfold periodicEdgeInnerProduct5
 246  refine Finset.sum_congr rfl ?_
 247  intro e _
 248  ring
 249
 250theorem periodicEdgeInnerProduct5_zero_left
 251    (η : PeriodicEdgePerturbation5) :
 252    periodicEdgeInnerProduct5 (fun _ => 0) η = 0 := by
 253  simp [periodicEdgeInnerProduct5]
 254
 255theorem periodicEdgeInnerProduct5_zero_right
 256    (ε : PeriodicEdgePerturbation5) :
 257    periodicEdgeInnerProduct5 ε (fun _ => 0) = 0 := by
 258  simp [periodicEdgeInnerProduct5]
 259
 260theorem periodicEdgeInnerProduct5_add_right
 261    (ε η ζ : PeriodicEdgePerturbation5) :
 262    periodicEdgeInnerProduct5 ε (fun e => η e + ζ e) =
 263      periodicEdgeInnerProduct5 ε η + periodicEdgeInnerProduct5 ε ζ := by
 264  unfold periodicEdgeInnerProduct5
 265  rw [← Finset.sum_add_distrib]
 266  refine Finset.sum_congr rfl ?_
 267  intro e _
 268  ring
 269
 270set_option maxRecDepth 65536
 271
 272/-- On the finite real periodic-edge space, zero self-inner-product forces the
 273edge perturbation itself to vanish. -/
 274theorem periodicEdgePerturbation5_eq_zero_of_inner_self_eq_zero
 275    (ε : PeriodicEdgePerturbation5)
 276    (h : periodicEdgeInnerProduct5 ε ε = 0) :
 277    ε = fun _ => 0 := by
 278  funext e
 279  have hsum : (∑ x : PeriodicEdge5, ε x * ε x) = 0 := by
 280    simpa [periodicEdgeInnerProduct5] using h
 281  by_contra hne
 282  have hpos : 0 < ε e * ε e := mul_self_pos.mpr hne
 283  have hsum_pos : 0 < ∑ x : PeriodicEdge5, ε x * ε x := by
 284    exact Finset.sum_pos'
 285      (fun x _ => mul_self_nonneg (ε x))
 286      ⟨e, Finset.mem_univ e, hpos⟩
 287  rw [hsum] at hsum_pos
 288  exact (lt_irrefl (0 : ℝ) hsum_pos).elim
 289
 290/-- The periodic-edge version of the vertex-conformal/log-strain subspace. -/
 291def PeriodicConformalLogSubspace5
 292    (ε : PeriodicEdgePerturbation5) : Prop :=
 293  ∃ ξ : VertexPotential PeriodicTorus5.K,
 294    ε = encodedToPeriodicEdgePerturbation5 (conformalEdgeLogStrain PeriodicTorus5.K ξ)
 295
 296theorem periodicConformalLogSubspace5_zero :
 297    PeriodicConformalLogSubspace5 (fun _ => 0) := by
 298  refine ⟨fun _ => 0, ?_⟩
 299  funext e
 300  simp [encodedToPeriodicEdgePerturbation5, conformalEdgeLogStrain]
 301
 302/-- Encoded vertex delta used to generate the finite conformal subspace. -/
 303def encodedVertexDeltaPotential5
 304    (v : Fin PeriodicTorus5.K.nV) : VertexPotential PeriodicTorus5.K :=
 305  fun w => if w = v then 1 else 0
 306
 307/-- The conformal generator obtained by putting unit potential at one encoded
 308vertex and zero potential at the others. -/
 309def periodicConformalGenerator5
 310    (v : Fin PeriodicTorus5.K.nV) : PeriodicEdgePerturbation5 :=
 311  encodedToPeriodicEdgePerturbation5
 312    (conformalEdgeLogStrain PeriodicTorus5.K (encodedVertexDeltaPotential5 v))
 313
 314/-- Pointwise form of the conformal vertex-delta edge generator in typed
 315periodic-edge coordinates. -/
 316theorem periodicConformalGenerator5_apply_endpoint
 317    (v : Fin PeriodicTorus5.K.nV) (e : PeriodicEdge5) :
 318    periodicConformalGenerator5 v e =
 319      ((if periodicVertexEquiv5.symm e.endpoints.1 = v then 1 else 0) +
 320        (if periodicVertexEquiv5.symm e.endpoints.2 = v then 1 else 0)) / 2 := by
 321  unfold periodicConformalGenerator5 encodedToPeriodicEdgePerturbation5
 322    conformalEdgeLogStrain encodedVertexDeltaPotential5
 323  rw [periodicTorus5_edgeVerts_symm_eq_endpoints]
 324
 325/-- The concrete `N = 5` conformal slice is spanned by encoded vertex delta
 326generators.  This supplies the conformal half of the finite-generator TT
 327projector data. -/
 328theorem periodicConformalLogSubspace5_spanned_by_encodedVertexGenerators
 329    (c : PeriodicEdgePerturbation5)
 330    (hc : PeriodicConformalLogSubspace5 c) :
 331    ∃ coeff : Fin PeriodicTorus5.K.nV → ℝ,
 332      ∀ e, c e = ∑ v : Fin PeriodicTorus5.K.nV,
 333        coeff v * periodicConformalGenerator5 v e := by
 334  classical
 335  rcases hc with ⟨ξ, rfl⟩
 336  refine ⟨ξ, ?_⟩
 337  intro e
 338  unfold periodicConformalGenerator5 encodedVertexDeltaPotential5
 339    encodedToPeriodicEdgePerturbation5 conformalEdgeLogStrain
 340  simp [Finset.mul_sum, Finset.sum_add_distrib, div_eq_mul_inv, mul_add,
 341    mul_assoc, mul_comm]
 342
 343/-- A gauge subspace supplied by a concrete forward Track 1.D gauge operator. The
 344operator remains a parameter here, so this file does not pretend to have already
 345chosen the longitudinal/diffeomorphism discretization. -/
 346def PeriodicGaugeSubspace5
 347    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5)
 348    (ε : PeriodicEdgePerturbation5) : Prop :=
 349  ∃ A : GaugePotential, ε = gaugeMap A
 350
 351/-- TT means orthogonal to the conformal slice and to the supplied gauge slice
 352with respect to the finite periodic-edge inner product. -/
 353def PeriodicTTOrthogonal5
 354    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5)
 355    (ε : PeriodicEdgePerturbation5) : Prop :=
 356  (∀ c : PeriodicEdgePerturbation5,
 357      PeriodicConformalLogSubspace5 c → periodicEdgeInnerProduct5 ε c = 0) ∧
 358  (∀ g : PeriodicEdgePerturbation5,
 359      PeriodicGaugeSubspace5 GaugePotential gaugeMap g →
 360        periodicEdgeInnerProduct5 ε g = 0)
 361
 362theorem periodicTTOrthogonal5_zero
 363    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5) :
 364    PeriodicTTOrthogonal5 GaugePotential gaugeMap (fun _ => 0) := by
 365  constructor
 366  · intro c _
 367    exact periodicEdgeInnerProduct5_zero_left c
 368  · intro g _
 369    exact periodicEdgeInnerProduct5_zero_left g
 370
 371/-- Honest Track 1.D decomposition target with TT interpreted as finite
 372orthogonality to the conformal and gauge subspaces.  The remaining mathematical
 373load is the construction of the three projectors. -/
 374def PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
 375    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5) : Prop :=
 376  ∃ split : RawEdgePerturbationSplitting PeriodicEdge5,
 377    (∀ ε, PeriodicConformalLogSubspace5 (split.conformalPart ε)) ∧
 378    (∀ ε, PeriodicGaugeSubspace5 GaugePotential gaugeMap (split.gaugePart ε)) ∧
 379    (∀ ε, PeriodicTTOrthogonal5 GaugePotential gaugeMap (split.ttPart ε))
 380
 381/-- Concrete projector data needed to close the finite `N = 5` conformal/gauge/TT
 382decomposition.  This is still a theorem-shaped target: the tensor lane must
 383construct these three maps for the chosen gauge operator and prove membership
 384plus pointwise reconstruction. -/
 385structure PeriodicTTProjectorData5
 386    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5) where
 387  conformalProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 388  gaugeProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 389  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 390  conformal_mem :
 391    ∀ ε, PeriodicConformalLogSubspace5 (conformalProjector ε)
 392  gauge_mem :
 393    ∀ ε, PeriodicGaugeSubspace5 GaugePotential gaugeMap (gaugeProjector ε)
 394  tt_mem :
 395    ∀ ε, PeriodicTTOrthogonal5 GaugePotential gaugeMap (ttProjector ε)
 396  reconstruct :
 397    ∀ ε e, conformalProjector ε e + gaugeProjector ε e + ttProjector ε e = ε e
 398
 399/-- Linearity of the finite periodic-edge inner product in the right argument,
 400specialized to a finite linear combination. -/
 401theorem periodicEdgeInnerProduct5_linear_combo_right
 402    {ι : Type} [Fintype ι]
 403    (ε : PeriodicEdgePerturbation5)
 404    (coeff : ι → ℝ) (basis : ι → PeriodicEdgePerturbation5) :
 405    periodicEdgeInnerProduct5 ε (fun e => ∑ i : ι, coeff i * basis i e) =
 406      ∑ i : ι, coeff i * periodicEdgeInnerProduct5 ε (basis i) := by
 407  classical
 408  unfold periodicEdgeInnerProduct5
 409  calc
 410    (∑ e : PeriodicEdge5, ε e * (∑ i : ι, coeff i * basis i e)) =
 411        ∑ e : PeriodicEdge5, ∑ i : ι, ε e * (coeff i * basis i e) := by
 412          refine Finset.sum_congr rfl ?_
 413          intro e _
 414          rw [Finset.mul_sum]
 415    _ = ∑ i : ι, ∑ e : PeriodicEdge5, ε e * (coeff i * basis i e) := by
 416          rw [Finset.sum_comm]
 417    _ = ∑ i : ι, coeff i * ∑ e : PeriodicEdge5, ε e * basis i e := by
 418          refine Finset.sum_congr rfl ?_
 419          intro i _
 420          rw [Finset.mul_sum]
 421          refine Finset.sum_congr rfl ?_
 422          intro e _
 423          ring
 424
 425/-- Finite-generator projector data.  This is the next concrete Track 1.D proof
 426surface: give finite spanning families for the conformal and gauge slices, then
 427construct projectors whose TT residual is orthogonal to every generator. -/
 428structure PeriodicTTFiniteGeneratorProjectorData5
 429    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5)
 430    (CIdx GIdx : Type) [Fintype CIdx] [Fintype GIdx] where
 431  conformalProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 432  gaugeProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 433  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 434  conformalGen : CIdx → PeriodicEdgePerturbation5
 435  gaugeGen : GIdx → PeriodicEdgePerturbation5
 436  conformal_mem :
 437    ∀ ε, PeriodicConformalLogSubspace5 (conformalProjector ε)
 438  gauge_mem :
 439    ∀ ε, PeriodicGaugeSubspace5 GaugePotential gaugeMap (gaugeProjector ε)
 440  conformal_span :
 441    ∀ c, PeriodicConformalLogSubspace5 c →
 442      ∃ coeff : CIdx → ℝ, ∀ e, c e = ∑ i : CIdx, coeff i * conformalGen i e
 443  gauge_span :
 444    ∀ g, PeriodicGaugeSubspace5 GaugePotential gaugeMap g →
 445      ∃ coeff : GIdx → ℝ, ∀ e, g e = ∑ i : GIdx, coeff i * gaugeGen i e
 446  tt_orthogonal_conformal_gen :
 447    ∀ ε i, periodicEdgeInnerProduct5 (ttProjector ε) (conformalGen i) = 0
 448  tt_orthogonal_gauge_gen :
 449    ∀ ε i, periodicEdgeInnerProduct5 (ttProjector ε) (gaugeGen i) = 0
 450  reconstruct :
 451    ∀ ε e, conformalProjector ε e + gaugeProjector ε e + ttProjector ε e = ε e
 452
 453/-- The gauge map generated by a finite family of longitudinal edge
 454perturbations.  Gauge potentials are coefficient vectors on the supplied
 455generators. -/
 456def periodicGaugeGeneratorMap5
 457    {GIdx : Type} [Fintype GIdx]
 458    (gaugeGen : GIdx → PeriodicEdgePerturbation5) :
 459    (GIdx → ℝ) → PeriodicEdgePerturbation5 :=
 460  fun coeff e => ∑ i : GIdx, coeff i * gaugeGen i e
 461
 462/-- The conformal projector generated by coefficients on the encoded vertex
 463delta basis. -/
 464def periodicConformalGeneratorMap5 :
 465    (Fin PeriodicTorus5.K.nV → ℝ) → PeriodicEdgePerturbation5 :=
 466  periodicGaugeGeneratorMap5 periodicConformalGenerator5
 467
 468/-- The conformal generator map has two-point support on a concrete edge: only
 469the base and head endpoint coefficients contribute. -/
 470theorem periodicConformalGeneratorMap5_apply_endpoint
 471    (coeff : Fin PeriodicTorus5.K.nV → ℝ) (e : PeriodicEdge5) :
 472    periodicConformalGeneratorMap5 coeff e =
 473      (coeff (periodicVertexEquiv5.symm e.endpoints.1) +
 474        coeff (periodicVertexEquiv5.symm e.endpoints.2)) / 2 := by
 475  classical
 476  unfold periodicConformalGeneratorMap5 periodicGaugeGeneratorMap5
 477  simp [periodicConformalGenerator5_apply_endpoint, Finset.sum_add_distrib,
 478    div_eq_mul_inv, mul_add, mul_comm]
 479
 480/-- Any coefficient vector on the encoded vertex-delta conformal generators
 481lands in the conformal subspace. -/
 482theorem periodicConformalGeneratorMap5_mem
 483    (coeff : Fin PeriodicTorus5.K.nV → ℝ) :
 484    PeriodicConformalLogSubspace5 (periodicConformalGeneratorMap5 coeff) := by
 485  classical
 486  refine ⟨coeff, ?_⟩
 487  funext e
 488  unfold periodicConformalGeneratorMap5 periodicGaugeGeneratorMap5
 489    periodicConformalGenerator5 encodedVertexDeltaPotential5
 490    encodedToPeriodicEdgePerturbation5 conformalEdgeLogStrain
 491  simp [Finset.mul_sum, Finset.sum_add_distrib, div_eq_mul_inv, mul_add,
 492    mul_assoc, mul_comm]
 493
 494/-- The image of a generator-defined gauge map is spanned by its generators by
 495construction. -/
 496theorem periodicGaugeSubspace5_spanned_by_generatorMap
 497    {GIdx : Type} [Fintype GIdx]
 498    (gaugeGen : GIdx → PeriodicEdgePerturbation5)
 499    (g : PeriodicEdgePerturbation5)
 500    (hg : PeriodicGaugeSubspace5 (GIdx → ℝ) (periodicGaugeGeneratorMap5 gaugeGen) g) :
 501    ∃ coeff : GIdx → ℝ, ∀ e, g e = ∑ i : GIdx, coeff i * gaugeGen i e := by
 502  rcases hg with ⟨coeff, rfl⟩
 503  exact ⟨coeff, fun _ => rfl⟩
 504
 505/-- Index type for the concrete periodic longitudinal gauge basis: one vector
 506component at one periodic vertex. -/
 507abbrev PeriodicLongitudinalGaugeIdx5 :=
 508  PeriodicVertex5 × Fin 3
 509
 510/-- Translate a concrete longitudinal gauge basis index by a typed row base. -/
 511def periodicTranslateLongitudinalGaugeIdx5
 512    (base : PeriodicVertex5) (idx : PeriodicLongitudinalGaugeIdx5) :
 513    PeriodicLongitudinalGaugeIdx5 :=
 514  (periodicTranslateVertex5 base idx.1, idx.2)
 515
 516/-- Coordinate component of one of the seven positive Freudenthal edge
 517displacements. -/
 518def periodicDispCoord5 (disp : Fin 7) (j : Fin 3) : ℝ :=
 519  let bits := dispBits disp
 520  match j with
 521  | ⟨0, _⟩ => if bits.1 then 1 else 0
 522  | ⟨1, _⟩ => if bits.2.1 then 1 else 0
 523  | ⟨2, _⟩ => if bits.2.2 then 1 else 0
 524
 525/-- Concrete finite longitudinal gauge generator on periodic edge strains.  It is
 526the signed edge-direction component of a unit vector field at one vertex:
 527positive at the head endpoint and negative at the base endpoint. -/
 528def periodicLongitudinalGaugeGenerator5
 529    (idx : PeriodicLongitudinalGaugeIdx5) : PeriodicEdgePerturbation5 :=
 530  fun e =>
 531    let d := periodicDispCoord5 e.disp idx.2
 532    (if e.endpoints.2 = idx.1 then d else 0) -
 533      (if e.endpoints.1 = idx.1 then d else 0)
 534
 535/-- The concrete finite longitudinal gauge map generated by vertex-vector delta
 536basis elements. -/
 537def periodicLongitudinalGaugeMap5 :
 538    (PeriodicLongitudinalGaugeIdx5 → ℝ) → PeriodicEdgePerturbation5 :=
 539  periodicGaugeGeneratorMap5 periodicLongitudinalGaugeGenerator5
 540
 541/-- The longitudinal gauge map has endpoint support on a concrete edge: only
 542the three component coefficients at the edge base and head contribute. -/
 543theorem periodicLongitudinalGaugeMap5_apply_endpoint
 544    (coeff : PeriodicLongitudinalGaugeIdx5 → ℝ) (e : PeriodicEdge5) :
 545    periodicLongitudinalGaugeMap5 coeff e =
 546      ∑ c : Fin 3,
 547        (coeff (e.endpoints.2, c) - coeff (e.endpoints.1, c)) *
 548          periodicDispCoord5 e.disp c := by
 549  classical
 550  unfold periodicLongitudinalGaugeMap5 periodicGaugeGeneratorMap5
 551    periodicLongitudinalGaugeGenerator5
 552  rw [Fintype.sum_prod_type]
 553  simp [Finset.sum_sub_distrib, mul_sub, mul_comm]
 554
 555/-- The concrete longitudinal gauge map is, by definition, generated by the
 556vertex-vector longitudinal basis. -/
 557theorem periodicLongitudinalGaugeMap5_eq_generatorMap :
 558    periodicLongitudinalGaugeMap5 =
 559      periodicGaugeGeneratorMap5 periodicLongitudinalGaugeGenerator5 :=
 560  rfl
 561
 562/-- Concrete TT predicate for the fixed longitudinal-gauge tensor sector. -/
 563abbrev PeriodicLongitudinalTTSubspace5 :=
 564  PeriodicTTOrthogonal5
 565    (PeriodicLongitudinalGaugeIdx5 → ℝ)
 566    periodicLongitudinalGaugeMap5
 567
 568/-- The concrete longitudinal gauge image is spanned by the vertex-vector delta
 569generators. -/
 570theorem periodicGaugeSubspace5_spanned_by_longitudinalGeneratorMap
 571    (g : PeriodicEdgePerturbation5)
 572    (hg : PeriodicGaugeSubspace5
 573      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 g) :
 574    ∃ coeff : PeriodicLongitudinalGaugeIdx5 → ℝ,
 575      ∀ e, g e =
 576        ∑ i : PeriodicLongitudinalGaugeIdx5,
 577          coeff i * periodicLongitudinalGaugeGenerator5 i e := by
 578  exact periodicGaugeSubspace5_spanned_by_generatorMap
 579    periodicLongitudinalGaugeGenerator5 g hg
 580
 581/-- Gauge-generator projector data, with the conformal generators fixed to the
 582encoded vertex-delta family already proved to span the conformal slice.  This is
 583the sharper Track 1.D target after the conformal half has been discharged. -/
 584structure PeriodicTTGaugeGeneratorProjectorData5
 585    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5)
 586    (GIdx : Type) [Fintype GIdx] where
 587  conformalProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 588  gaugeProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 589  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 590  gaugeGen : GIdx → PeriodicEdgePerturbation5
 591  conformal_mem :
 592    ∀ ε, PeriodicConformalLogSubspace5 (conformalProjector ε)
 593  gauge_mem :
 594    ∀ ε, PeriodicGaugeSubspace5 GaugePotential gaugeMap (gaugeProjector ε)
 595  gauge_span :
 596    ∀ g, PeriodicGaugeSubspace5 GaugePotential gaugeMap g →
 597      ∃ coeff : GIdx → ℝ, ∀ e, g e = ∑ i : GIdx, coeff i * gaugeGen i e
 598  tt_orthogonal_conformal_gen :
 599    ∀ ε v, periodicEdgeInnerProduct5 (ttProjector ε) (periodicConformalGenerator5 v) = 0
 600  tt_orthogonal_gauge_gen :
 601    ∀ ε i, periodicEdgeInnerProduct5 (ttProjector ε) (gaugeGen i) = 0
 602  reconstruct :
 603    ∀ ε e, conformalProjector ε e + gaugeProjector ε e + ttProjector ε e = ε e
 604
 605/-- Projector data for a gauge map that is itself defined by finite generators.
 606This removes a separate gauge-span obligation: the gauge map is the span. -/
 607structure PeriodicTTGeneratorMapProjectorData5
 608    (GIdx : Type) [Fintype GIdx] where
 609  conformalProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 610  gaugeCoeffProjector : PeriodicEdgePerturbation5 → GIdx → ℝ
 611  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 612  gaugeGen : GIdx → PeriodicEdgePerturbation5
 613  conformal_mem :
 614    ∀ ε, PeriodicConformalLogSubspace5 (conformalProjector ε)
 615  tt_orthogonal_conformal_gen :
 616    ∀ ε v, periodicEdgeInnerProduct5 (ttProjector ε) (periodicConformalGenerator5 v) = 0
 617  tt_orthogonal_gauge_gen :
 618    ∀ ε i, periodicEdgeInnerProduct5 (ttProjector ε) (gaugeGen i) = 0
 619  reconstruct :
 620    ∀ ε e,
 621      conformalProjector ε e +
 622        periodicGaugeGeneratorMap5 gaugeGen (gaugeCoeffProjector ε) e +
 623        ttProjector ε e = ε e
 624
 625/-- Projector data for the concrete periodic longitudinal gauge basis.  This is
 626now the exact finite-dimensional decomposition input still owed by Track 1.D. -/
 627structure PeriodicTTLongitudinalProjectorData5 where
 628  conformalProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 629  gaugeCoeffProjector :
 630    PeriodicEdgePerturbation5 → PeriodicLongitudinalGaugeIdx5 → ℝ
 631  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 632  conformal_mem :
 633    ∀ ε, PeriodicConformalLogSubspace5 (conformalProjector ε)
 634  tt_orthogonal_conformal_gen :
 635    ∀ ε v, periodicEdgeInnerProduct5 (ttProjector ε) (periodicConformalGenerator5 v) = 0
 636  tt_orthogonal_gauge_gen :
 637    ∀ ε i,
 638      periodicEdgeInnerProduct5 (ttProjector ε) (periodicLongitudinalGaugeGenerator5 i) = 0
 639  reconstruct :
 640    ∀ ε e,
 641      conformalProjector ε e +
 642        periodicLongitudinalGaugeMap5 (gaugeCoeffProjector ε) e +
 643        ttProjector ε e = ε e
 644
 645/-- Pure coefficient-projector data for the concrete longitudinal split.  The
 646conformal part is no longer an arbitrary map: it is explicitly generated from
 647encoded vertex-delta coefficients. -/
 648structure PeriodicTTLongitudinalCoefficientProjectorData5 where
 649  conformalCoeffProjector :
 650    PeriodicEdgePerturbation5 → Fin PeriodicTorus5.K.nV → ℝ
 651  gaugeCoeffProjector :
 652    PeriodicEdgePerturbation5 → PeriodicLongitudinalGaugeIdx5 → ℝ
 653  ttProjector : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
 654  tt_orthogonal_conformal_gen :
 655    ∀ ε v, periodicEdgeInnerProduct5 (ttProjector ε) (periodicConformalGenerator5 v) = 0
 656  tt_orthogonal_gauge_gen :
 657    ∀ ε i,
 658      periodicEdgeInnerProduct5 (ttProjector ε) (periodicLongitudinalGaugeGenerator5 i) = 0
 659  reconstruct :
 660    ∀ ε e,
 661      periodicConformalGeneratorMap5 (conformalCoeffProjector ε) e +
 662        periodicLongitudinalGaugeMap5 (gaugeCoeffProjector ε) e +
 663        ttProjector ε e = ε e
 664
 665/-- Residual after subtracting the conformal and longitudinal coefficient
 666projections from an edge perturbation. -/
 667def periodicLongitudinalCoefficientResidual5
 668    (conformalCoeffProjector :
 669      PeriodicEdgePerturbation5 → Fin PeriodicTorus5.K.nV → ℝ)
 670    (gaugeCoeffProjector :
 671      PeriodicEdgePerturbation5 → PeriodicLongitudinalGaugeIdx5 → ℝ)
 672    (ε : PeriodicEdgePerturbation5) : PeriodicEdgePerturbation5 :=
 673  fun e =>
 674    ε e - periodicConformalGeneratorMap5 (conformalCoeffProjector ε) e -
 675      periodicLongitudinalGaugeMap5 (gaugeCoeffProjector ε) e
 676
 677/-- The coefficient solve can be stated with no separate TT projector: the TT
 678part is the residual after subtracting the conformal and longitudinal projections. -/
 679structure PeriodicTTLongitudinalCoefficientSolutionData5 where
 680  conformalCoeffProjector :
 681    PeriodicEdgePerturbation5 → Fin PeriodicTorus5.K.nV → ℝ
 682  gaugeCoeffProjector :
 683    PeriodicEdgePerturbation5 → PeriodicLongitudinalGaugeIdx5 → ℝ
 684  residual_orthogonal_conformal_gen :
 685    ∀ ε v,
 686      periodicEdgeInnerProduct5
 687        (periodicLongitudinalCoefficientResidual5
 688          conformalCoeffProjector gaugeCoeffProjector ε)
 689        (periodicConformalGenerator5 v) = 0
 690  residual_orthogonal_gauge_gen :
 691    ∀ ε i,
 692      periodicEdgeInnerProduct5
 693        (periodicLongitudinalCoefficientResidual5
 694          conformalCoeffProjector gaugeCoeffProjector ε)
 695        (periodicLongitudinalGaugeGenerator5 i) = 0
 696
 697/-- Combined index for the fixed conformal vertex-delta generators and fixed
 698longitudinal vertex-vector generators. -/
 699abbrev PeriodicTTNormalEquationIdx5 :=
 700  Sum (Fin PeriodicTorus5.K.nV) PeriodicLongitudinalGaugeIdx5
 701
 702/-- Translate a combined normal-equation generator index by a typed row base.
 703Conformal indices use the encoded vertex equivalence; gauge indices translate
 704the vertex and preserve the vector component. -/
 705noncomputable def periodicTranslateTTNormalEquationIdx5
 706    (base : PeriodicVertex5) :
 707    PeriodicTTNormalEquationIdx5 → PeriodicTTNormalEquationIdx5
 708  | Sum.inl v => Sum.inl (periodicTranslateEncodedVertexIdx5 base v)
 709  | Sum.inr i => Sum.inr (periodicTranslateLongitudinalGaugeIdx5 base i)
 710
 711/-- Combined generator family for the concrete finite TT normal equations. -/
 712def periodicTTNormalEquationGenerator5
 713    (idx : PeriodicTTNormalEquationIdx5) : PeriodicEdgePerturbation5 :=
 714  match idx with
 715  | Sum.inl v => periodicConformalGenerator5 v
 716  | Sum.inr i => periodicLongitudinalGaugeGenerator5 i
 717
 718/-- Conformal coefficients extracted from a combined coefficient vector. -/
 719def periodicTTNormalEquationConformalCoeff5
 720    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
 721    Fin PeriodicTorus5.K.nV → ℝ :=
 722  fun v => coeff (Sum.inl v)
 723
 724/-- Longitudinal coefficients extracted from a combined coefficient vector. -/
 725def periodicTTNormalEquationGaugeCoeff5
 726    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
 727    PeriodicLongitudinalGaugeIdx5 → ℝ :=
 728  fun i => coeff (Sum.inr i)
 729
 730/-- Combined generator map for the concrete finite TT normal equations. -/
 731def periodicTTNormalEquationGeneratorMap5 :
 732    (PeriodicTTNormalEquationIdx5 → ℝ) → PeriodicEdgePerturbation5 :=
 733  periodicGaugeGeneratorMap5 periodicTTNormalEquationGenerator5
 734
 735/-- External-order displacement component used by the numerical TT
 736normal-equation generator matrix. -/
 737def periodicExternalDispCoordNat5 (disp : Fin 7) (component : Nat) : ℝ :=
 738  let bits := dispBits disp
 739  match component with
 740  | 0 => if bits.1 then 1 else 0
 741  | 1 => if bits.2.1 then 1 else 0
 742  | 2 => if bits.2.2 then 1 else 0
 743  | _ => 0
 744
 745/-- External-order head vertex index for a typed edge. -/
 746def periodicExternalEdgeHeadIndex5 (e : PeriodicEdge5) : Nat :=
 747  periodicExternalVertexIndex5 e.endpoints.2
 748
 749/-- Entry of the external TT normal-equation generator matrix used by the
 750Python payloads. Rows are external edge indices; columns `0..124` are
 751conformal vertex deltas and columns `125..499` are longitudinal
 752vertex-component generators. -/
 753def periodicExternalTTNormalEquationGeneratorMatrixEntry5
 754    (edgeIdx : Fin PeriodicTorus5.K.nE) (col : Nat) : ℝ :=
 755  let e := periodicExternalEdgeOfEncodedIdx5 edgeIdx
 756  let baseIdx := periodicExternalVertexIndex5 e.endpoints.1
 757  let headIdx := periodicExternalEdgeHeadIndex5 e
 758  if col < 125 then
 759    ((if col = baseIdx then 1 else 0) + (if col = headIdx then 1 else 0)) / 2
 760  else
 761    let gaugeCol := col - 125
 762    let vertexIdx := gaugeCol / 3
 763    let component := gaugeCol % 3
 764    (if vertexIdx = headIdx then periodicExternalDispCoordNat5 e.disp component else 0) -
 765      (if vertexIdx = baseIdx then periodicExternalDispCoordNat5 e.disp component else 0)
 766
 767/-- External generator-matrix dot product for one selected row. This is the
 768Lean-side counterpart of the Python matrix dot used by generated certificate
 769skeletons. -/
 770def periodicExternalTTNormalEquationGeneratorMatrixDot5
 771    (coeff : Nat → ℝ) (edgeIdx : Fin PeriodicTorus5.K.nE) : ℝ :=
 772  ∑ col : Fin 500,
 773    coeff col.1 * periodicExternalTTNormalEquationGeneratorMatrixEntry5 edgeIdx col.1
 774
 775/-- Sparse external generator-matrix dot product for one selected row. This is
 776definitionally small: two conformal endpoint terms plus the three possible
 777longitudinal component differences. -/
 778def periodicExternalTTNormalEquationGeneratorSparseDot5
 779    (coeff : Nat → ℝ) (edgeIdx : Fin PeriodicTorus5.K.nE) : ℝ :=
 780  let e := periodicExternalEdgeOfEncodedIdx5 edgeIdx
 781  let baseIdx := periodicExternalVertexIndex5 e.endpoints.1
 782  let headIdx := periodicExternalEdgeHeadIndex5 e
 783  (coeff baseIdx + coeff headIdx) / 2 +
 784    ((coeff (125 + 3 * headIdx + 0) -
 785        coeff (125 + 3 * baseIdx + 0)) *
 786      periodicExternalDispCoordNat5 e.disp 0) +
 787    ((coeff (125 + 3 * headIdx + 1) -
 788        coeff (125 + 3 * baseIdx + 1)) *
 789      periodicExternalDispCoordNat5 e.disp 1) +
 790    ((coeff (125 + 3 * headIdx + 2) -
 791        coeff (125 + 3 * baseIdx + 2)) *
 792      periodicExternalDispCoordNat5 e.disp 2)
 793
 794/-- The combined normal-equation generator map splits into the already-fixed
 795conformal and longitudinal generator maps. -/
 796theorem periodicTTNormalEquationGeneratorMap5_eq_split
 797    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) (e : PeriodicEdge5) :
 798    periodicTTNormalEquationGeneratorMap5 coeff e =
 799      periodicConformalGeneratorMap5
 800        (periodicTTNormalEquationConformalCoeff5 coeff) e +
 801      periodicLongitudinalGaugeMap5
 802        (periodicTTNormalEquationGaugeCoeff5 coeff) e := by
 803  classical
 804  unfold periodicTTNormalEquationGeneratorMap5 periodicConformalGeneratorMap5
 805    periodicLongitudinalGaugeMap5 periodicGaugeGeneratorMap5
 806    periodicTTNormalEquationConformalCoeff5 periodicTTNormalEquationGaugeCoeff5
 807    periodicTTNormalEquationGenerator5
 808  rw [Fintype.sum_sum_type]
 809
 810/-- Right-hand side of the concrete TT normal equations: pair the input edge
 811perturbation with each combined generator. -/
 812def periodicTTNormalEquationLoad5
 813    (ε : PeriodicEdgePerturbation5) (idx : PeriodicTTNormalEquationIdx5) : ℝ :=
 814  periodicEdgeInnerProduct5 ε (periodicTTNormalEquationGenerator5 idx)
 815
 816/-- Gram operator for the fixed combined conformal plus longitudinal generator
 817family. -/
 818def periodicTTNormalEquationGramApply5
 819    (coeff : PeriodicTTNormalEquationIdx5 → ℝ)
 820    (idx : PeriodicTTNormalEquationIdx5) : ℝ :=
 821  ∑ j : PeriodicTTNormalEquationIdx5,
 822    coeff j *
 823      periodicEdgeInnerProduct5
 824        (periodicTTNormalEquationGenerator5 idx)
 825        (periodicTTNormalEquationGenerator5 j)
 826
 827/-- The Gram operator is exactly the inner product against the combined
 828generator map. -/
 829theorem periodicTTNormalEquationGramApply5_eq_inner_generatorMap
 830    (coeff : PeriodicTTNormalEquationIdx5 → ℝ)
 831    (idx : PeriodicTTNormalEquationIdx5) :
 832    periodicTTNormalEquationGramApply5 coeff idx =
 833      periodicEdgeInnerProduct5
 834        (periodicTTNormalEquationGenerator5 idx)
 835        (periodicTTNormalEquationGeneratorMap5 coeff) := by
 836  unfold periodicTTNormalEquationGramApply5 periodicTTNormalEquationGeneratorMap5
 837    periodicGaugeGeneratorMap5
 838  rw [periodicEdgeInnerProduct5_linear_combo_right]
 839
 840/-- Residual for a combined finite normal-equation coefficient projector. -/
 841def periodicTTNormalEquationResidual5
 842    (coeffProjector :
 843      PeriodicEdgePerturbation5 → PeriodicTTNormalEquationIdx5 → ℝ)
 844    (ε : PeriodicEdgePerturbation5) : PeriodicEdgePerturbation5 :=
 845  periodicLongitudinalCoefficientResidual5
 846    (fun ε => periodicTTNormalEquationConformalCoeff5 (coeffProjector ε))
 847    (fun ε => periodicTTNormalEquationGaugeCoeff5 (coeffProjector ε))
 848    ε
 849
 850/-- The combined normal-equation residual is the input minus the combined
 851generator-map reconstruction. -/
 852theorem periodicTTNormalEquationResidual5_eq_sub_generatorMap
 853    (coeffProjector :
 854      PeriodicEdgePerturbation5 → PeriodicTTNormalEquationIdx5 → ℝ)
 855    (ε : PeriodicEdgePerturbation5) (e : PeriodicEdge5) :
 856    periodicTTNormalEquationResidual5 coeffProjector ε e =
 857      ε e - periodicTTNormalEquationGeneratorMap5 (coeffProjector ε) e := by
 858  unfold periodicTTNormalEquationResidual5 periodicLongitudinalCoefficientResidual5
 859  rw [periodicTTNormalEquationGeneratorMap5_eq_split]
 860  ring
 861
 862/-- Pairing the combined residual with a generator is exactly load minus Gram. -/
 863theorem periodicTTNormalEquationResidual_inner_eq_load_sub_gram
 864    (coeffProjector :
 865      PeriodicEdgePerturbation5 → PeriodicTTNormalEquationIdx5 → ℝ)
 866    (ε : PeriodicEdgePerturbation5) (idx : PeriodicTTNormalEquationIdx5) :
 867    periodicEdgeInnerProduct5
 868      (periodicTTNormalEquationResidual5 coeffProjector ε)
 869      (periodicTTNormalEquationGenerator5 idx) =
 870      periodicTTNormalEquationLoad5 ε idx -
 871        periodicTTNormalEquationGramApply5 (coeffProjector ε) idx := by
 872  classical
 873  calc
 874    periodicEdgeInnerProduct5
 875        (periodicTTNormalEquationResidual5 coeffProjector ε)
 876        (periodicTTNormalEquationGenerator5 idx)
 877        =
 878        periodicEdgeInnerProduct5
 879          (fun e =>
 880            ε e - periodicTTNormalEquationGeneratorMap5 (coeffProjector ε) e)
 881          (periodicTTNormalEquationGenerator5 idx) := by
 882          unfold periodicEdgeInnerProduct5
 883          refine Finset.sum_congr rfl ?_
 884          intro e _
 885          rw [periodicTTNormalEquationResidual5_eq_sub_generatorMap]
 886    _ =
 887        periodicTTNormalEquationLoad5 ε idx -
 888          periodicEdgeInnerProduct5
 889            (periodicTTNormalEquationGeneratorMap5 (coeffProjector ε))
 890            (periodicTTNormalEquationGenerator5 idx) := by
 891          unfold periodicEdgeInnerProduct5 periodicTTNormalEquationLoad5
 892          calc
 893            (∑ e : PeriodicEdge5,
 894                (fun e =>
 895                  ε e - periodicTTNormalEquationGeneratorMap5 (coeffProjector ε) e) e *
 896                  periodicTTNormalEquationGenerator5 idx e)
 897                =
 898                ∑ e : PeriodicEdge5,
 899                  (ε e * periodicTTNormalEquationGenerator5 idx e -
 900                    periodicTTNormalEquationGeneratorMap5 (coeffProjector ε) e *
 901                      periodicTTNormalEquationGenerator5 idx e) := by
 902                  refine Finset.sum_congr rfl ?_
 903                  intro e _
 904                  ring
 905            _ =
 906                (∑ e : PeriodicEdge5,
 907                  ε e * periodicTTNormalEquationGenerator5 idx e) -
 908                ∑ e : PeriodicEdge5,
 909                  periodicTTNormalEquationGeneratorMap5 (coeffProjector ε) e *
 910                    periodicTTNormalEquationGenerator5 idx e := by
 911                  rw [Finset.sum_sub_distrib]
 912    _ =
 913        periodicTTNormalEquationLoad5 ε idx -
 914          periodicEdgeInnerProduct5
 915            (periodicTTNormalEquationGenerator5 idx)
 916            (periodicTTNormalEquationGeneratorMap5 (coeffProjector ε)) := by
 917          rw [periodicEdgeInnerProduct5_symm]
 918    _ =
 919        periodicTTNormalEquationLoad5 ε idx -
 920          periodicTTNormalEquationGramApply5 (coeffProjector ε) idx := by
 921          rw [← periodicTTNormalEquationGramApply5_eq_inner_generatorMap]
 922
 923/-- Single-system normal-equation data for the concrete finite TT split.  This is
 924the finite linear-algebra problem left by the decomposition track. -/
 925structure PeriodicTTNormalEquationSolutionData5 where
 926  coeffProjector :
 927    PeriodicEdgePerturbation5 → PeriodicTTNormalEquationIdx5 → ℝ
 928  normal_equations :
 929    ∀ ε idx,
 930      periodicEdgeInnerProduct5
 931        (periodicTTNormalEquationResidual5 coeffProjector ε)
 932        (periodicTTNormalEquationGenerator5 idx) = 0
 933
 934/-- Explicit Gram-system solution data for the concrete finite TT split. -/
 935structure PeriodicTTGramSystemSolutionData5 where
 936  coeffProjector :
 937    PeriodicEdgePerturbation5 → PeriodicTTNormalEquationIdx5 → ℝ
 938  gram_system :
 939    ∀ ε idx,
 940      periodicTTNormalEquationGramApply5 (coeffProjector ε) idx =
 941        periodicTTNormalEquationLoad5 ε idx
 942
 943/-- Load-solver data for the finite TT Gram operator.  This isolates the
 944remaining finite linear-algebra work: solve the Gram system for every load
 945vector arising from an edge perturbation. -/
 946structure PeriodicTTGramLoadSolverData5 where
 947  loadSolver :
 948    (PeriodicTTNormalEquationIdx5 → ℝ) → PeriodicTTNormalEquationIdx5 → ℝ
 949  solves_loads :
 950    ∀ ε idx,
 951      periodicTTNormalEquationGramApply5
 952          (loadSolver (periodicTTNormalEquationLoad5 ε)) idx =
 953        periodicTTNormalEquationLoad5 ε idx
 954
 955/-- Image/range data for the finite TT Gram operator.  This is weaker and more
 956geometric than choosing a solver: every load generated by an edge perturbation
 957must lie in the image of the fixed Gram operator. -/
 958structure PeriodicTTGramLoadImageData5 where
 959  load_mem_image :
 960    ∀ ε,
 961      ∃ coeff : PeriodicTTNormalEquationIdx5 → ℝ,
 962        ∀ idx,
 963          periodicTTNormalEquationGramApply5 coeff idx =
 964            periodicTTNormalEquationLoad5 ε idx
 965
 966/-- Coefficient-space inner product on the finite normal-equation index set. -/
 967def periodicTTNormalEquationCoeffInnerProduct5
 968    (a b : PeriodicTTNormalEquationIdx5 → ℝ) : ℝ :=
 969  ∑ idx : PeriodicTTNormalEquationIdx5, a idx * b idx
 970
 971/-- Coefficient-vector space for the combined conformal plus longitudinal normal
 972equations. -/
 973abbrev PeriodicTTCoeffSpace5 :=
 974  PeriodicTTNormalEquationIdx5 → ℝ
 975
 976/-- `WithLp 2` Hilbert wrapper for the finite coefficient-vector space.  The raw
 977coefficient type intentionally stays a function space elsewhere in the file;
 978this wrapper imports Mathlib's inner-product range theorem without changing the
 979public TT data surfaces. -/
 980abbrev PeriodicTTCoeffHilbertSpace5 :=
 981  WithLp 2 PeriodicTTCoeffSpace5
 982
 983/-- Linear equivalence between the Hilbert wrapper and the raw coefficient
 984function space. -/
 985noncomputable abbrev periodicTTCoeffHilbertEquiv5 :
 986    PeriodicTTCoeffHilbertSpace5 ≃ₗ[ℝ] PeriodicTTCoeffSpace5 :=
 987  WithLp.linearEquiv 2 ℝ PeriodicTTCoeffSpace5
 988
 989/-- Gram operator as a coefficient vector. -/
 990def periodicTTNormalEquationGramVector5
 991    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
 992    PeriodicTTNormalEquationIdx5 → ℝ :=
 993  fun idx => periodicTTNormalEquationGramApply5 coeff idx
 994
 995/-- The TT Gram operator as a linear map on raw coefficient functions. -/
 996noncomputable def periodicTTGramLinearMap5 :
 997    PeriodicTTCoeffSpace5 →ₗ[ℝ] PeriodicTTCoeffSpace5 where
 998  toFun := periodicTTNormalEquationGramVector5
 999  map_add' := by
1000    intro a b
1001    funext idx
1002    unfold periodicTTNormalEquationGramVector5 periodicTTNormalEquationGramApply5
1003    simp [Pi.add_apply, add_mul, Finset.sum_add_distrib]
1004  map_smul' := by
1005    intro c a
1006    funext idx
1007    unfold periodicTTNormalEquationGramVector5 periodicTTNormalEquationGramApply5
1008    simp only [Pi.smul_apply, smul_eq_mul, RingHom.id_apply]
1009    rw [Finset.mul_sum]
1010    refine Finset.sum_congr rfl ?_
1011    intro j _
1012    ring
1013
1014/-- The TT Gram operator transported to Mathlib's finite Hilbert wrapper. -/
1015noncomputable def periodicTTGramHilbertLinearMap5 :
1016    PeriodicTTCoeffHilbertSpace5 →ₗ[ℝ] PeriodicTTCoeffHilbertSpace5 :=
1017  periodicTTCoeffHilbertEquiv5.symm.toLinearMap.comp
1018    (periodicTTGramLinearMap5.comp periodicTTCoeffHilbertEquiv5.toLinearMap)
1019
1020/-- The Hilbert-wrapper inner product is the coefficient-space dot product. -/
1021theorem periodicTTCoeffHilbert_inner_eq_coeffInnerProduct5
1022    (a b : PeriodicTTCoeffSpace5) :
1023    inner ℝ
1024      (periodicTTCoeffHilbertEquiv5.symm a)
1025      (periodicTTCoeffHilbertEquiv5.symm b) =
1026      periodicTTNormalEquationCoeffInnerProduct5 a b := by
1027  simp [periodicTTNormalEquationCoeffInnerProduct5, PiLp.inner_apply, mul_comm]
1028
1029/-- Symmetry of the coefficient-space dot product. -/
1030theorem periodicTTNormalEquationCoeffInnerProduct5_symm
1031    (a b : PeriodicTTCoeffSpace5) :
1032    periodicTTNormalEquationCoeffInnerProduct5 a b =
1033      periodicTTNormalEquationCoeffInnerProduct5 b a := by
1034  unfold periodicTTNormalEquationCoeffInnerProduct5
1035  refine Finset.sum_congr rfl ?_
1036  intro idx _
1037  ring
1038
1039/-- Symmetric Gram entry identity for the combined generator family. -/
1040theorem periodicTTNormalEquationGramEntry_symm5
1041    (i j : PeriodicTTNormalEquationIdx5) :
1042    periodicEdgeInnerProduct5
1043      (periodicTTNormalEquationGenerator5 i)
1044      (periodicTTNormalEquationGenerator5 j) =
1045    periodicEdgeInnerProduct5
1046      (periodicTTNormalEquationGenerator5 j)
1047      (periodicTTNormalEquationGenerator5 i) :=
1048  periodicEdgeInnerProduct5_symm _ _
1049
1050/-- The finite TT Gram operator is self-adjoint for the coefficient inner
1051product. -/
1052theorem periodicTTNormalEquationGram_selfAdjoint5
1053    (a b : PeriodicTTNormalEquationIdx5 → ℝ) :
1054    periodicTTNormalEquationCoeffInnerProduct5
1055      (periodicTTNormalEquationGramVector5 a) b =
1056    periodicTTNormalEquationCoeffInnerProduct5
1057      a (periodicTTNormalEquationGramVector5 b) := by
1058  classical
1059  unfold periodicTTNormalEquationCoeffInnerProduct5
1060    periodicTTNormalEquationGramVector5 periodicTTNormalEquationGramApply5
1061  calc
1062    (∑ i : PeriodicTTNormalEquationIdx5,
1063        (∑ j : PeriodicTTNormalEquationIdx5,
1064          a j *
1065            periodicEdgeInnerProduct5
1066              (periodicTTNormalEquationGenerator5 i)
1067              (periodicTTNormalEquationGenerator5 j)) * b i)
1068        =
1069        ∑ i : PeriodicTTNormalEquationIdx5,
1070          ∑ j : PeriodicTTNormalEquationIdx5,
1071            a j * b i *
1072              periodicEdgeInnerProduct5
1073                (periodicTTNormalEquationGenerator5 i)
1074                (periodicTTNormalEquationGenerator5 j) := by
1075          refine Finset.sum_congr rfl ?_
1076          intro i _
1077          rw [Finset.sum_mul]
1078          refine Finset.sum_congr rfl ?_
1079          intro j _
1080          ring
1081    _ =
1082        ∑ j : PeriodicTTNormalEquationIdx5,
1083          ∑ i : PeriodicTTNormalEquationIdx5,
1084            a j * b i *
1085              periodicEdgeInnerProduct5
1086                (periodicTTNormalEquationGenerator5 i)
1087                (periodicTTNormalEquationGenerator5 j) := by
1088          rw [Finset.sum_comm]
1089    _ =
1090        ∑ j : PeriodicTTNormalEquationIdx5,
1091          ∑ i : PeriodicTTNormalEquationIdx5,
1092            a j * b i *
1093              periodicEdgeInnerProduct5
1094                (periodicTTNormalEquationGenerator5 j)
1095                (periodicTTNormalEquationGenerator5 i) := by
1096          refine Finset.sum_congr rfl ?_
1097          intro j _
1098          refine Finset.sum_congr rfl ?_
1099          intro i _
1100          rw [periodicTTNormalEquationGramEntry_symm5 i j]
1101    _ =
1102        ∑ j : PeriodicTTNormalEquationIdx5,
1103          a j *
1104            ∑ i : PeriodicTTNormalEquationIdx5,
1105              b i *
1106                periodicEdgeInnerProduct5
1107                  (periodicTTNormalEquationGenerator5 j)
1108                  (periodicTTNormalEquationGenerator5 i) := by
1109          refine Finset.sum_congr rfl ?_
1110          intro j _
1111          rw [Finset.mul_sum]
1112          refine Finset.sum_congr rfl ?_
1113          intro i _
1114          ring
1115
1116set_option maxRecDepth 20000
1117
1118/-- The transported finite TT Gram operator is symmetric in Mathlib's Hilbert
1119wrapper. -/
1120theorem periodicTTGramHilbertLinearMap_isSymmetric5 :
1121    LinearMap.IsSymmetric periodicTTGramHilbertLinearMap5 := by
1122  intro x y
1123  unfold periodicTTGramHilbertLinearMap5
1124  simp only [LinearMap.comp_apply, LinearEquiv.coe_coe]
1125  rw [show
1126      inner ℝ
1127        (periodicTTCoeffHilbertEquiv5.symm
1128          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 x))) y =
1129        periodicTTNormalEquationCoeffInnerProduct5
1130          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 x))
1131          (periodicTTCoeffHilbertEquiv5 y) by
1132      simpa using
1133        periodicTTCoeffHilbert_inner_eq_coeffInnerProduct5
1134          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 x))
1135          (periodicTTCoeffHilbertEquiv5 y)]
1136  rw [show
1137      inner ℝ x
1138        (periodicTTCoeffHilbertEquiv5.symm
1139          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 y))) =
1140        periodicTTNormalEquationCoeffInnerProduct5
1141          (periodicTTCoeffHilbertEquiv5 x)
1142          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 y)) by
1143      simpa using
1144        periodicTTCoeffHilbert_inner_eq_coeffInnerProduct5
1145          (periodicTTCoeffHilbertEquiv5 x)
1146          (periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 y))]
1147  exact
1148    periodicTTNormalEquationGram_selfAdjoint5
1149      (periodicTTCoeffHilbertEquiv5 x)
1150      (periodicTTCoeffHilbertEquiv5 y)
1151
1152/-- Kernel of the finite TT Gram operator. -/
1153def periodicTTGramKernel5
1154    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) : Prop :=
1155  ∀ idx, periodicTTNormalEquationGramApply5 coeff idx = 0
1156
1157/-- A Gram-kernel coefficient vector generates the zero edge perturbation. -/
1158theorem periodicTTGramKernel_generatorMap_zero5
1159    (coeff : PeriodicTTNormalEquationIdx5 → ℝ)
1160    (hkernel : periodicTTGramKernel5 coeff) :
1161    periodicTTNormalEquationGeneratorMap5 coeff = fun _ => 0 := by
1162  apply periodicEdgePerturbation5_eq_zero_of_inner_self_eq_zero
1163  calc
1164    periodicEdgeInnerProduct5
1165        (periodicTTNormalEquationGeneratorMap5 coeff)
1166        (periodicTTNormalEquationGeneratorMap5 coeff)
1167        =
1168        periodicEdgeInnerProduct5
1169          (periodicTTNormalEquationGeneratorMap5 coeff)
1170          (fun e =>
1171            ∑ idx : PeriodicTTNormalEquationIdx5,
1172              coeff idx * periodicTTNormalEquationGenerator5 idx e) := by
1173          rfl
1174    _ =
1175        ∑ idx : PeriodicTTNormalEquationIdx5,
1176          coeff idx *
1177            periodicEdgeInnerProduct5
1178              (periodicTTNormalEquationGeneratorMap5 coeff)
1179              (periodicTTNormalEquationGenerator5 idx) := by
1180          rw [periodicEdgeInnerProduct5_linear_combo_right]
1181    _ =
1182        ∑ idx : PeriodicTTNormalEquationIdx5,
1183          coeff idx *
1184            periodicEdgeInnerProduct5
1185              (periodicTTNormalEquationGenerator5 idx)
1186              (periodicTTNormalEquationGeneratorMap5 coeff) := by
1187          refine Finset.sum_congr rfl ?_
1188          intro idx _
1189          rw [periodicEdgeInnerProduct5_symm]
1190    _ =
1191        ∑ idx : PeriodicTTNormalEquationIdx5,
1192          coeff idx * periodicTTNormalEquationGramApply5 coeff idx := by
1193          refine Finset.sum_congr rfl ?_
1194          intro idx _
1195          rw [periodicTTNormalEquationGramApply5_eq_inner_generatorMap]
1196    _ = ∑ idx : PeriodicTTNormalEquationIdx5, coeff idx * 0 := by
1197          refine Finset.sum_congr rfl ?_
1198          intro idx _
1199          rw [hkernel idx, mul_zero]
1200    _ = 0 := by
1201          simp
1202
1203/-- The load induced by an edge perturbation annihilates every Gram-kernel
1204coefficient vector. -/
1205def periodicTTLoadAnnihilatesGramKernel5
1206    (ε : PeriodicEdgePerturbation5) : Prop :=
1207  ∀ kernelCoeff,
1208    periodicTTGramKernel5 kernelCoeff →
1209      periodicTTNormalEquationCoeffInnerProduct5
1210        (periodicTTNormalEquationLoad5 ε) kernelCoeff = 0
1211
1212/-- Pairing the load vector with coefficients is the edge inner product against
1213the combined generated mode. -/
1214theorem periodicTTLoadCoeffInnerProduct_eq_inner_generatorMap5
1215    (ε : PeriodicEdgePerturbation5)
1216    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
1217    periodicTTNormalEquationCoeffInnerProduct5
1218      (periodicTTNormalEquationLoad5 ε) coeff =
1219      periodicEdgeInnerProduct5 ε (periodicTTNormalEquationGeneratorMap5 coeff) := by
1220  classical
1221  unfold periodicTTNormalEquationCoeffInnerProduct5 periodicTTNormalEquationLoad5
1222    periodicTTNormalEquationGeneratorMap5 periodicGaugeGeneratorMap5
1223  rw [periodicEdgeInnerProduct5_linear_combo_right]
1224  refine Finset.sum_congr rfl ?_
1225  intro idx _
1226  ring
1227
1228/-- A longitudinal TT perturbation is orthogonal to every combined conformal
1229plus longitudinal normal-equation generator map. -/
1230theorem periodicLongitudinalTTSubspace5_inner_generatorMap_eq_zero
1231    (ε : PeriodicEdgePerturbation5)
1232    (hε :
1233      PeriodicTTOrthogonal5
1234        (PeriodicLongitudinalGaugeIdx5 → ℝ)
1235        periodicLongitudinalGaugeMap5 ε)
1236    (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
1237    periodicEdgeInnerProduct5 ε
1238      (periodicTTNormalEquationGeneratorMap5 coeff) = 0 := by
1239  let cCoeff := periodicTTNormalEquationConformalCoeff5 coeff
1240  let gCoeff := periodicTTNormalEquationGaugeCoeff5 coeff
1241  have hmap :
1242      periodicTTNormalEquationGeneratorMap5 coeff =
1243        fun e =>
1244          periodicConformalGeneratorMap5 cCoeff e +
1245            periodicLongitudinalGaugeMap5 gCoeff e := by
1246    funext e
1247    exact periodicTTNormalEquationGeneratorMap5_eq_split coeff e
1248  rw [hmap]
1249  rw [periodicEdgeInnerProduct5_add_right]
1250  have hc :
1251      periodicEdgeInnerProduct5 ε
1252        (periodicConformalGeneratorMap5 cCoeff) = 0 :=
1253    hε.1 (periodicConformalGeneratorMap5 cCoeff)
1254      (periodicConformalGeneratorMap5_mem cCoeff)
1255  have hg :
1256      periodicEdgeInnerProduct5 ε
1257        (periodicLongitudinalGaugeMap5 gCoeff) = 0 :=
1258    hε.2 (periodicLongitudinalGaugeMap5 gCoeff) ⟨gCoeff, rfl⟩
1259  rw [hc, hg]
1260  ring
1261
1262/-- Kernel-criterion data for the finite TT Gram operator.  This is the finite
1263Fredholm-alternative surface: to prove the loads are in the Gram image, it is
1264enough to prove they annihilate the Gram kernel, together with the finite
1265range criterion for this fixed Gram operator. -/
1266structure PeriodicTTGramKernelCriterionData5 where
1267  range_of_kernel_orthogonal :
1268    ∀ load : PeriodicTTNormalEquationIdx5 → ℝ,
1269      (∀ kernelCoeff,
1270        periodicTTGramKernel5 kernelCoeff →
1271          periodicTTNormalEquationCoeffInnerProduct5 load kernelCoeff = 0) →
1272        ∃ coeff : PeriodicTTNormalEquationIdx5 → ℝ,
1273          ∀ idx, periodicTTNormalEquationGramApply5 coeff idx = load idx
1274  loads_annihilate_kernel :
1275    ∀ ε, periodicTTLoadAnnihilatesGramKernel5 ε
1276
1277/-- Kernel-zero-mode data for the TT Gram operator.  This leaves only the finite
1278range criterion plus the statement that every Gram-kernel coefficient vector
1279generates the zero edge perturbation. -/
1280structure PeriodicTTGramKernelGeneratorMapZeroData5 where
1281  range_of_kernel_orthogonal :
1282    ∀ load : PeriodicTTNormalEquationIdx5 → ℝ,
1283      (∀ kernelCoeff,
1284        periodicTTGramKernel5 kernelCoeff →
1285          periodicTTNormalEquationCoeffInnerProduct5 load kernelCoeff = 0) →
1286        ∃ coeff : PeriodicTTNormalEquationIdx5 → ℝ,
1287          ∀ idx, periodicTTNormalEquationGramApply5 coeff idx = load idx
1288  kernel_generatorMap_zero :
1289    ∀ coeff,
1290      periodicTTGramKernel5 coeff →
1291        periodicTTNormalEquationGeneratorMap5 coeff = fun _ => 0
1292
1293/-- Range-criterion data for the finite TT Gram operator.  Since Gram-kernel
1294coefficient vectors now theorematically generate the zero edge perturbation, the
1295only remaining finite-algebra input is this range/Fredholm criterion for the
1296fixed Gram operator. -/
1297structure PeriodicTTGramRangeCriterionData5 where
1298  range_of_kernel_orthogonal :
1299    ∀ load : PeriodicTTNormalEquationIdx5 → ℝ,
1300      (∀ kernelCoeff,
1301        periodicTTGramKernel5 kernelCoeff →
1302          periodicTTNormalEquationCoeffInnerProduct5 load kernelCoeff = 0) →
1303        ∃ coeff : PeriodicTTNormalEquationIdx5 → ℝ,
1304          ∀ idx, periodicTTNormalEquationGramApply5 coeff idx = load idx
1305
1306/-- The fixed finite TT Gram range/Fredholm criterion is theorem-level.  This is
1307the finite-dimensional fact that a load orthogonal to the Gram kernel lies in
1308the range of the self-adjoint Gram operator. -/
1309theorem periodicTTGramRangeCriterionData5_proved :
1310    PeriodicTTGramRangeCriterionData5 := by
1311  refine ⟨?_⟩
1312  intro load hload
1313  let loadH : PeriodicTTCoeffHilbertSpace5 :=
1314    periodicTTCoeffHilbertEquiv5.symm load
1315  have hkerOrth :
1316      loadH ∈ (LinearMap.ker periodicTTGramHilbertLinearMap5)ᗮ := by
1317    rw [Submodule.mem_orthogonal]
1318    intro u hu
1319    rw [LinearMap.mem_ker] at hu
1320    have hraw_zero :
1321        periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 u) = 0 := by
1322      have hcongr := congrArg periodicTTCoeffHilbertEquiv5 hu
1323      simpa [periodicTTGramHilbertLinearMap5] using hcongr
1324    have hkernel :
1325        periodicTTGramKernel5 (periodicTTCoeffHilbertEquiv5 u) := by
1326      intro idx
1327      have hidx := congrFun hraw_zero idx
1328      simpa [periodicTTGramLinearMap5, periodicTTNormalEquationGramVector5] using hidx
1329    have hcustom :
1330        periodicTTNormalEquationCoeffInnerProduct5
1331          load (periodicTTCoeffHilbertEquiv5 u) = 0 :=
1332      hload (periodicTTCoeffHilbertEquiv5 u) hkernel
1333    calc
1334      inner ℝ u loadH =
1335          periodicTTNormalEquationCoeffInnerProduct5
1336            (periodicTTCoeffHilbertEquiv5 u) load := by
1337        simpa [loadH] using
1338          periodicTTCoeffHilbert_inner_eq_coeffInnerProduct5
1339            (periodicTTCoeffHilbertEquiv5 u) load
1340      _ =
1341          periodicTTNormalEquationCoeffInnerProduct5
1342            load (periodicTTCoeffHilbertEquiv5 u) :=
1343        periodicTTNormalEquationCoeffInnerProduct5_symm
1344          (periodicTTCoeffHilbertEquiv5 u) load
1345      _ = 0 := hcustom
1346  have horthRange :
1347      (LinearMap.range periodicTTGramHilbertLinearMap5)ᗮ =
1348        LinearMap.ker periodicTTGramHilbertLinearMap5 :=
1349    LinearMap.IsSymmetric.orthogonal_range periodicTTGramHilbertLinearMap_isSymmetric5
1350  have hmemDouble :
1351      loadH ∈ (LinearMap.range periodicTTGramHilbertLinearMap5)ᗮᗮ := by
1352    simpa [horthRange] using hkerOrth
1353  have hdouble :
1354      (LinearMap.range periodicTTGramHilbertLinearMap5)ᗮᗮ =
1355        LinearMap.range periodicTTGramHilbertLinearMap5 := by
1356    rw [Submodule.orthogonal_orthogonal_eq_closure]
1357    exact Submodule.topologicalClosure_eq_self
1358      (LinearMap.range periodicTTGramHilbertLinearMap5)
1359  have hmemRange :
1360      loadH ∈ LinearMap.range periodicTTGramHilbertLinearMap5 := by
1361    simpa [hdouble] using hmemDouble
1362  rcases LinearMap.mem_range.mp hmemRange with ⟨coeffH, hcoeffH⟩
1363  refine ⟨periodicTTCoeffHilbertEquiv5 coeffH, ?_⟩
1364  intro idx
1365  have hraw :
1366      periodicTTGramLinearMap5 (periodicTTCoeffHilbertEquiv5 coeffH) = load := by
1367    have hcongr := congrArg periodicTTCoeffHilbertEquiv5 hcoeffH
1368    simpa [periodicTTGramHilbertLinearMap5, loadH] using hcongr
1369  have hidx := congrFun hraw idx
1370  simpa [periodicTTGramLinearMap5, periodicTTNormalEquationGramVector5] using hidx
1371
1372/-- Generator-map projector data is gauge-generator projector data for the gauge
1373map induced by the same generator family. -/
1374def PeriodicTTGaugeGeneratorProjectorData5.ofGeneratorMapData
1375    {GIdx : Type} [Fintype GIdx]
1376    (D : PeriodicTTGeneratorMapProjectorData5 GIdx) :
1377    PeriodicTTGaugeGeneratorProjectorData5
1378      (GIdx → ℝ) (periodicGaugeGeneratorMap5 D.gaugeGen) GIdx where
1379  conformalProjector := D.conformalProjector
1380  gaugeProjector := fun ε => periodicGaugeGeneratorMap5 D.gaugeGen (D.gaugeCoeffProjector ε)
1381  ttProjector := D.ttProjector
1382  gaugeGen := D.gaugeGen
1383  conformal_mem := D.conformal_mem
1384  gauge_mem := by
1385    intro ε
1386    exact ⟨D.gaugeCoeffProjector ε, rfl⟩
1387  gauge_span := periodicGaugeSubspace5_spanned_by_generatorMap D.gaugeGen
1388  tt_orthogonal_conformal_gen := D.tt_orthogonal_conformal_gen
1389  tt_orthogonal_gauge_gen := D.tt_orthogonal_gauge_gen
1390  reconstruct := D.reconstruct
1391
1392/-- Concrete longitudinal projector data is generator-map projector data for the
1393longitudinal vertex-vector basis. -/
1394def PeriodicTTGeneratorMapProjectorData5.ofLongitudinalData
1395    (D : PeriodicTTLongitudinalProjectorData5) :
1396    PeriodicTTGeneratorMapProjectorData5 PeriodicLongitudinalGaugeIdx5 where
1397  conformalProjector := D.conformalProjector
1398  gaugeCoeffProjector := D.gaugeCoeffProjector
1399  ttProjector := D.ttProjector
1400  gaugeGen := periodicLongitudinalGaugeGenerator5
1401  conformal_mem := D.conformal_mem
1402  tt_orthogonal_conformal_gen := D.tt_orthogonal_conformal_gen
1403  tt_orthogonal_gauge_gen := D.tt_orthogonal_gauge_gen
1404  reconstruct := by
1405    intro ε e
1406    exact D.reconstruct ε e
1407
1408/-- Coefficient-projector data supplies the concrete longitudinal projector data
1409by generating the conformal part from encoded vertex-delta coefficients. -/
1410def PeriodicTTLongitudinalProjectorData5.ofCoefficientData
1411    (D : PeriodicTTLongitudinalCoefficientProjectorData5) :
1412    PeriodicTTLongitudinalProjectorData5 where
1413  conformalProjector := fun ε => periodicConformalGeneratorMap5 (D.conformalCoeffProjector ε)
1414  gaugeCoeffProjector := D.gaugeCoeffProjector
1415  ttProjector := D.ttProjector
1416  conformal_mem := fun ε => periodicConformalGeneratorMap5_mem (D.conformalCoeffProjector ε)
1417  tt_orthogonal_conformal_gen := D.tt_orthogonal_conformal_gen
1418  tt_orthogonal_gauge_gen := D.tt_orthogonal_gauge_gen
1419  reconstruct := D.reconstruct
1420
1421/-- Residual-defined coefficient-solution data supplies the coefficient-projector
1422data expected by the decomposition target. -/
1423def PeriodicTTLongitudinalCoefficientProjectorData5.ofSolutionData
1424    (D : PeriodicTTLongitudinalCoefficientSolutionData5) :
1425    PeriodicTTLongitudinalCoefficientProjectorData5 where
1426  conformalCoeffProjector := D.conformalCoeffProjector
1427  gaugeCoeffProjector := D.gaugeCoeffProjector
1428  ttProjector :=
1429    periodicLongitudinalCoefficientResidual5
1430      D.conformalCoeffProjector D.gaugeCoeffProjector
1431  tt_orthogonal_conformal_gen := D.residual_orthogonal_conformal_gen
1432  tt_orthogonal_gauge_gen := D.residual_orthogonal_gauge_gen
1433  reconstruct := by
1434    intro ε e
1435    unfold periodicLongitudinalCoefficientResidual5
1436    ring
1437
1438/-- A solution of the combined normal equations supplies the residual-defined
1439coefficient solution data. -/
1440def PeriodicTTLongitudinalCoefficientSolutionData5.ofNormalEquationData
1441    (D : PeriodicTTNormalEquationSolutionData5) :
1442    PeriodicTTLongitudinalCoefficientSolutionData5 where
1443  conformalCoeffProjector :=
1444    fun ε => periodicTTNormalEquationConformalCoeff5 (D.coeffProjector ε)
1445  gaugeCoeffProjector :=
1446    fun ε => periodicTTNormalEquationGaugeCoeff5 (D.coeffProjector ε)
1447  residual_orthogonal_conformal_gen := by
1448    intro ε v
1449    simpa [periodicTTNormalEquationResidual5, periodicTTNormalEquationGenerator5]
1450      using D.normal_equations ε (Sum.inl v)
1451  residual_orthogonal_gauge_gen := by
1452    intro ε i
1453    simpa [periodicTTNormalEquationResidual5, periodicTTNormalEquationGenerator5]
1454      using D.normal_equations ε (Sum.inr i)
1455
1456/-- Solving the explicit Gram system supplies the combined normal equations. -/
1457def PeriodicTTNormalEquationSolutionData5.ofGramSystemData
1458    (D : PeriodicTTGramSystemSolutionData5) :
1459    PeriodicTTNormalEquationSolutionData5 where
1460  coeffProjector := D.coeffProjector
1461  normal_equations := by
1462    intro ε idx
1463    rw [periodicTTNormalEquationResidual_inner_eq_load_sub_gram]
1464    rw [D.gram_system ε idx]
1465    ring
1466
1467/-- A load solver supplies the explicit Gram-system solution data. -/
1468def PeriodicTTGramSystemSolutionData5.ofLoadSolverData
1469    (D : PeriodicTTGramLoadSolverData5) :
1470    PeriodicTTGramSystemSolutionData5 where
1471  coeffProjector := fun ε => D.loadSolver (periodicTTNormalEquationLoad5 ε)
1472  gram_system := D.solves_loads
1473
1474/-- Load-image data supplies a solver on the physical load subspace by choosing a
1475preimage for each load that actually occurs. -/
1476noncomputable def PeriodicTTGramLoadSolverData5.ofLoadImageData
1477    (D : PeriodicTTGramLoadImageData5) :
1478    PeriodicTTGramLoadSolverData5 where
1479  loadSolver := by
1480    classical
1481    exact fun load =>
1482      if h : ∃ ε, load = periodicTTNormalEquationLoad5 ε then
1483        Classical.choose (D.load_mem_image (Classical.choose h))
1484      else
1485        fun _ => 0
1486  solves_loads := by
1487    intro ε idx
1488    classical
1489    let h : ∃ η, periodicTTNormalEquationLoad5 ε = periodicTTNormalEquationLoad5 η :=
1490      ⟨ε, rfl⟩
1491    rw [dif_pos h]
1492    have hload :
1493        periodicTTNormalEquationLoad5 ε =
1494          periodicTTNormalEquationLoad5 (Classical.choose h) :=
1495      Classical.choose_spec h
1496    exact
1497      (Classical.choose_spec (D.load_mem_image (Classical.choose h)) idx).trans
1498        ((congrFun hload idx).symm)
1499
1500/-- The kernel criterion supplies the load-image data required by the finite TT
1501decomposition target. -/
1502def PeriodicTTGramLoadImageData5.ofKernelCriterionData
1503    (D : PeriodicTTGramKernelCriterionData5) :
1504    PeriodicTTGramLoadImageData5 where
1505  load_mem_image := by
1506    intro ε
1507    exact D.range_of_kernel_orthogonal
1508      (periodicTTNormalEquationLoad5 ε)
1509      (D.loads_annihilate_kernel ε)
1510
1511/-- Kernel-generator-zero data supplies the finite Gram-kernel criterion. -/
1512def PeriodicTTGramKernelCriterionData5.ofKernelGeneratorMapZeroData
1513    (D : PeriodicTTGramKernelGeneratorMapZeroData5) :
1514    PeriodicTTGramKernelCriterionData5 where
1515  range_of_kernel_orthogonal := D.range_of_kernel_orthogonal
1516  loads_annihilate_kernel := by
1517    intro ε kernelCoeff hkernel
1518    rw [periodicTTLoadCoeffInnerProduct_eq_inner_generatorMap5]
1519    rw [D.kernel_generatorMap_zero kernelCoeff hkernel]
1520    exact periodicEdgeInnerProduct5_zero_right ε
1521
1522/-- The finite Gram range criterion alone now supplies the Gram-kernel criterion,
1523because Gram-kernel coefficients are proved to generate zero edge perturbations. -/
1524def PeriodicTTGramKernelCriterionData5.ofRangeCriterionData
1525    (D : PeriodicTTGramRangeCriterionData5) :
1526    PeriodicTTGramKernelCriterionData5 where
1527  range_of_kernel_orthogonal := D.range_of_kernel_orthogonal
1528  loads_annihilate_kernel := by
1529    intro ε kernelCoeff hkernel
1530    rw [periodicTTLoadCoeffInnerProduct_eq_inner_generatorMap5]
1531    rw [periodicTTGramKernel_generatorMap_zero5 kernelCoeff hkernel]
1532    exact periodicEdgeInnerProduct5_zero_right ε
1533
1534/-- Gauge-generator data is full finite-generator data, using encoded vertex
1535delta generators for the conformal slice. -/
1536def PeriodicTTFiniteGeneratorProjectorData5.ofGaugeGeneratorData
1537    {GaugePotential GIdx : Type} [Fintype GIdx]
1538    {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1539    (D : PeriodicTTGaugeGeneratorProjectorData5 GaugePotential gaugeMap GIdx) :
1540    PeriodicTTFiniteGeneratorProjectorData5
1541      GaugePotential gaugeMap (Fin PeriodicTorus5.K.nV) GIdx where
1542  conformalProjector := D.conformalProjector
1543  gaugeProjector := D.gaugeProjector
1544  ttProjector := D.ttProjector
1545  conformalGen := periodicConformalGenerator5
1546  gaugeGen := D.gaugeGen
1547  conformal_mem := D.conformal_mem
1548  gauge_mem := D.gauge_mem
1549  conformal_span := periodicConformalLogSubspace5_spanned_by_encodedVertexGenerators
1550  gauge_span := D.gauge_span
1551  tt_orthogonal_conformal_gen := D.tt_orthogonal_conformal_gen
1552  tt_orthogonal_gauge_gen := D.tt_orthogonal_gauge_gen
1553  reconstruct := D.reconstruct
1554
1555/-- Orthogonality to finite spanning generators gives full TT orthogonality. -/
1556theorem periodicTTOrthogonal5_of_generator_orthogonality
1557    {GaugePotential CIdx GIdx : Type} [Fintype CIdx] [Fintype GIdx]
1558    {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1559    (D : PeriodicTTFiniteGeneratorProjectorData5 GaugePotential gaugeMap CIdx GIdx)
1560    (ε : PeriodicEdgePerturbation5) :
1561    PeriodicTTOrthogonal5 GaugePotential gaugeMap (D.ttProjector ε) := by
1562  constructor
1563  · intro c hc
1564    rcases D.conformal_span c hc with ⟨coeff, hcoeff⟩
1565    have hc_eq : c = fun e => ∑ i : CIdx, coeff i * D.conformalGen i e := by
1566      funext e
1567      exact hcoeff e
1568    rw [hc_eq, periodicEdgeInnerProduct5_linear_combo_right]
1569    simp [D.tt_orthogonal_conformal_gen ε]
1570  · intro g hg
1571    rcases D.gauge_span g hg with ⟨coeff, hcoeff⟩
1572    have hg_eq : g = fun e => ∑ i : GIdx, coeff i * D.gaugeGen i e := by
1573      funext e
1574      exact hcoeff e
1575    rw [hg_eq, periodicEdgeInnerProduct5_linear_combo_right]
1576    simp [D.tt_orthogonal_gauge_gen ε]
1577
1578/-- Finite-generator projector data supplies the projector data consumed by the
1579orthogonal decomposition theorem. -/
1580def PeriodicTTProjectorData5.ofFiniteGeneratorData
1581    {GaugePotential CIdx GIdx : Type} [Fintype CIdx] [Fintype GIdx]
1582    {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1583    (D : PeriodicTTFiniteGeneratorProjectorData5 GaugePotential gaugeMap CIdx GIdx) :
1584    PeriodicTTProjectorData5 GaugePotential gaugeMap where
1585  conformalProjector := D.conformalProjector
1586  gaugeProjector := D.gaugeProjector
1587  ttProjector := D.ttProjector
1588  conformal_mem := D.conformal_mem
1589  gauge_mem := D.gauge_mem
1590  tt_mem := periodicTTOrthogonal5_of_generator_orthogonality D
1591  reconstruct := D.reconstruct
1592
1593/-- Projector data induces the raw additive splitting expected by the earlier
1594Track 1.D decomposition target. -/
1595def PeriodicTTProjectorData5.toRawSplitting
1596    {GaugePotential : Type} {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1597    (D : PeriodicTTProjectorData5 GaugePotential gaugeMap) :
1598    RawEdgePerturbationSplitting PeriodicEdge5 where
1599  conformalPart := D.conformalProjector
1600  gaugePart := D.gaugeProjector
1601  ttPart := D.ttProjector
1602  reconstruct := D.reconstruct
1603
1604/-- Projector data closes the finite orthogonal conformal/gauge/TT decomposition
1605target.  This is the intended next consumption theorem for a concrete periodic
1606Freudenthal projector construction. -/
1607theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_projectorData
1608    {GaugePotential : Type} {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1609    (D : PeriodicTTProjectorData5 GaugePotential gaugeMap) :
1610    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 GaugePotential gaugeMap := by
1611  refine ⟨D.toRawSplitting, ?_, ?_, ?_⟩
1612  · exact D.conformal_mem
1613  · exact D.gauge_mem
1614  · exact D.tt_mem
1615
1616/-- Finite-generator projector data closes the finite orthogonal decomposition
1617target.  The remaining tensor-lane task is now concrete: produce the generators,
1618solve the projector system, and prove reconstruction. -/
1619theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_finiteGeneratorData
1620    {GaugePotential CIdx GIdx : Type} [Fintype CIdx] [Fintype GIdx]
1621    {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1622    (D : PeriodicTTFiniteGeneratorProjectorData5 GaugePotential gaugeMap CIdx GIdx) :
1623    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 GaugePotential gaugeMap :=
1624  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_projectorData
1625    (PeriodicTTProjectorData5.ofFiniteGeneratorData D)
1626
1627/-- Gauge-generator projector data closes the finite orthogonal decomposition
1628target, because the conformal generators are fixed and already span. -/
1629theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gaugeGeneratorData
1630    {GaugePotential GIdx : Type} [Fintype GIdx]
1631    {gaugeMap : GaugePotential → PeriodicEdgePerturbation5}
1632    (D : PeriodicTTGaugeGeneratorProjectorData5 GaugePotential gaugeMap GIdx) :
1633    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 GaugePotential gaugeMap :=
1634  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_finiteGeneratorData
1635    (PeriodicTTFiniteGeneratorProjectorData5.ofGaugeGeneratorData D)
1636
1637/-- Generator-map projector data closes the finite orthogonal decomposition
1638target for the gauge map generated by its own finite basis. -/
1639theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_generatorMapData
1640    {GIdx : Type} [Fintype GIdx]
1641    (D : PeriodicTTGeneratorMapProjectorData5 GIdx) :
1642    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1643      (GIdx → ℝ) (periodicGaugeGeneratorMap5 D.gaugeGen) :=
1644  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gaugeGeneratorData
1645    (PeriodicTTGaugeGeneratorProjectorData5.ofGeneratorMapData D)
1646
1647/-- Concrete longitudinal projector data closes the finite TT decomposition
1648target for the vertex-vector longitudinal gauge map. -/
1649theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalData
1650    (D : PeriodicTTLongitudinalProjectorData5) :
1651    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1652      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 := by
1653  exact periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_generatorMapData
1654    (PeriodicTTGeneratorMapProjectorData5.ofLongitudinalData D)
1655
1656/-- Pure coefficient-projector data closes the concrete longitudinal TT
1657decomposition target. -/
1658theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalCoefficientData
1659    (D : PeriodicTTLongitudinalCoefficientProjectorData5) :
1660    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1661      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1662  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalData
1663    (PeriodicTTLongitudinalProjectorData5.ofCoefficientData D)
1664
1665/-- Residual-defined coefficient-solution data closes the concrete longitudinal
1666TT decomposition target. -/
1667theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalCoefficientSolutionData
1668    (D : PeriodicTTLongitudinalCoefficientSolutionData5) :
1669    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1670      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1671  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalCoefficientData
1672    (PeriodicTTLongitudinalCoefficientProjectorData5.ofSolutionData D)
1673
1674/-- A solution of the combined finite normal equations closes the concrete
1675longitudinal TT decomposition target. -/
1676theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_normalEquationData
1677    (D : PeriodicTTNormalEquationSolutionData5) :
1678    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1679      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1680  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_longitudinalCoefficientSolutionData
1681    (PeriodicTTLongitudinalCoefficientSolutionData5.ofNormalEquationData D)
1682
1683/-- A solution of the explicit finite Gram system closes the concrete
1684longitudinal TT decomposition target. -/
1685theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramSystemData
1686    (D : PeriodicTTGramSystemSolutionData5) :
1687    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1688      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1689  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_normalEquationData
1690    (PeriodicTTNormalEquationSolutionData5.ofGramSystemData D)
1691
1692/-- A finite load solver for the TT Gram operator closes the concrete
1693longitudinal TT decomposition target. -/
1694theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadSolverData
1695    (D : PeriodicTTGramLoadSolverData5) :
1696    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1697      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1698  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramSystemData
1699    (PeriodicTTGramSystemSolutionData5.ofLoadSolverData D)
1700
1701/-- If every physical load lies in the Gram image, the concrete longitudinal TT
1702decomposition target closes. -/
1703theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadImageData
1704    (D : PeriodicTTGramLoadImageData5) :
1705    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1706      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1707  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadSolverData
1708    (PeriodicTTGramLoadSolverData5.ofLoadImageData D)
1709
1710/-- The finite Gram-kernel criterion closes the concrete longitudinal TT
1711decomposition target. -/
1712theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData
1713    (D : PeriodicTTGramKernelCriterionData5) :
1714    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1715      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1716  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramLoadImageData
1717    (PeriodicTTGramLoadImageData5.ofKernelCriterionData D)
1718
1719/-- If Gram-kernel coefficient vectors generate zero edge perturbations, then the
1720finite Gram-kernel criterion closes the concrete longitudinal TT decomposition
1721target. -/
1722theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelGeneratorMapZeroData
1723    (D : PeriodicTTGramKernelGeneratorMapZeroData5) :
1724    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1725      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1726  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData
1727    (PeriodicTTGramKernelCriterionData5.ofKernelGeneratorMapZeroData D)
1728
1729/-- The finite Gram range criterion is enough to close the concrete longitudinal
1730TT decomposition target. -/
1731theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramRangeCriterionData
1732    (D : PeriodicTTGramRangeCriterionData5) :
1733    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1734      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1735  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramKernelCriterionData
1736    (PeriodicTTGramKernelCriterionData5.ofRangeCriterionData D)
1737
1738/-- The concrete longitudinal TT decomposition target is closed by the proved
1739finite Gram range theorem. -/
1740theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_provedGramRangeCriterion :
1741    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5
1742      (PeriodicLongitudinalGaugeIdx5 → ℝ) periodicLongitudinalGaugeMap5 :=
1743  periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_of_gramRangeCriterionData
1744    periodicTTGramRangeCriterionData5_proved
1745
1746/-! ## TT Hessian-to-Lichnerowicz matching surface -/
1747
1748/-- Bilinear form induced by an edge-space operator and the finite periodic-edge
1749inner product. -/
1750def periodicTTOperatorBilinear5
1751    (op : PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5)
1752    (ε η : PeriodicEdgePerturbation5) : ℝ :=
1753  periodicEdgeInnerProduct5 ε (op η)
1754
1755/-- Finite edge-kernel representation of an operator on periodic edge
1756perturbations.  This is the concrete matrix surface where the Regge TT Hessian
1757stencil and the lattice Lichnerowicz stencil should be compared. -/
1758abbrev PeriodicEdgeOperatorKernel5 :=
1759  PeriodicEdge5 → PeriodicEdge5 → ℝ
1760
1761/-- Encoded finite-triangulation version of an edge-kernel matrix.  This is the
1762native `Fin K.nE` index surface for kernels extracted from the encoded
1763Freudenthal triangulation. -/
1764abbrev EncodedEdgeOperatorKernel5 :=
1765  Fin PeriodicTorus5.K.nE → Fin PeriodicTorus5.K.nE → ℝ
1766
1767/-- Pull an encoded `Fin K.nE` edge kernel back to typed periodic-edge indices. -/
1768def encodedToPeriodicEdgeKernel5
1769    (kernel : EncodedEdgeOperatorKernel5) : PeriodicEdgeOperatorKernel5 :=
1770  fun e f => kernel (PeriodicTorus5.edgeEquiv.symm e) (PeriodicTorus5.edgeEquiv.symm f)
1771
1772theorem encodedToPeriodicEdgeKernel5_apply
1773    (kernel : EncodedEdgeOperatorKernel5) (e f : PeriodicEdge5) :
1774    encodedToPeriodicEdgeKernel5 kernel e f =
1775      kernel (PeriodicTorus5.edgeEquiv.symm e) (PeriodicTorus5.edgeEquiv.symm f) :=
1776  rfl
1777
1778/-- Difference kernel on the encoded finite edge-index surface. -/
1779def encodedEdgeKernelResidual5
1780    (reggeKernel lichnerowiczKernel : EncodedEdgeOperatorKernel5) :
1781    EncodedEdgeOperatorKernel5 :=
1782  fun e f => reggeKernel e f - lichnerowiczKernel e f
1783
1784theorem encodedEdgeKernelResidual5_apply
1785    (reggeKernel lichnerowiczKernel : EncodedEdgeOperatorKernel5)
1786    (e f : Fin PeriodicTorus5.K.nE) :
1787    encodedEdgeKernelResidual5 reggeKernel lichnerowiczKernel e f =
1788      reggeKernel e f - lichnerowiczKernel e f :=
1789  rfl
1790
1791/-- The origin vertex of the concrete `5 × 5 × 5` periodic torus. -/
1792def periodicOriginVertex5 : PeriodicVertex5 :=
1793  (0, 0, 0)
1794
1795/-- Coordinate subtraction on the concrete `N = 5` torus. -/
1796def periodicSubFin5 (base v : Fin 5) : Fin 5 :=
1797  ⟨(v.1 + (5 - base.1)) % 5, by omega⟩
1798
1799/-- Vertex coordinates of `v` in the frame whose origin is `base`. -/
1800def periodicRelativeVertex5 (base v : PeriodicVertex5) : PeriodicVertex5 :=
1801  (periodicSubFin5 base.1 v.1,
1802   periodicSubFin5 base.2.1 v.2.1,
1803   periodicSubFin5 base.2.2 v.2.2)
1804
1805theorem periodicRelativeVertex5_origin_eq_self (v : PeriodicVertex5) :
1806    periodicRelativeVertex5 periodicOriginVertex5 v = v := by
1807  rcases v with ⟨x, y, z⟩
1808  ext <;> simp [periodicRelativeVertex5, periodicSubFin5, periodicOriginVertex5]
1809
1810/-- Translating a relative-frame vertex back by its frame origin recovers the
1811original global vertex. -/
1812theorem periodicTranslateVertex5_relative_eq_self
1813    (base v : PeriodicVertex5) :
1814    periodicTranslateVertex5 base (periodicRelativeVertex5 base v) = v := by
1815  rcases base with ⟨bx, byz⟩
1816  rcases byz with ⟨byc, bz⟩
1817  rcases v with ⟨x, yz⟩
1818  rcases yz with ⟨y, z⟩
1819  ext <;> simp [periodicTranslateVertex5, periodicRelativeVertex5,
1820    periodicAddFin5, periodicSubFin5] <;> omega
1821
1822/-- Re-basing a translated vertex at the same origin recovers the original
1823relative vertex. -/
1824theorem periodicRelativeVertex5_translate_eq_self
1825    (base v : PeriodicVertex5) :
1826    periodicRelativeVertex5 base (periodicTranslateVertex5 base v) = v := by
1827  rcases base with ⟨bx, byz⟩
1828  rcases byz with ⟨byc, bz⟩
1829  rcases v with ⟨x, yz⟩
1830  rcases yz with ⟨y, z⟩
1831  ext <;> simp [periodicTranslateVertex5, periodicRelativeVertex5,
1832    periodicAddFin5, periodicSubFin5] <;> omega
1833
1834/-- Translation by a fixed periodic vertex is injective on the concrete torus. -/
1835theorem periodicTranslateVertex5_injective
1836    (base : PeriodicVertex5) :
1837    Function.Injective (periodicTranslateVertex5 base) := by
1838  intro v w h
1839  have hrel := congrArg (periodicRelativeVertex5 base) h
1840  simpa [periodicRelativeVertex5_translate_eq_self] using hrel
1841
1842/-- The origin-row representative for a periodic edge displacement. -/
1843def periodicOriginEdgeOfDisp5 (disp : Fin 7) : PeriodicEdge5 :=
1844  { base := periodicOriginVertex5, disp := disp }
1845
1846/-- Column edge written in the coordinate frame of a row edge. -/
1847def periodicRelativeColumnOfRow5
1848    (row col : PeriodicEdge5) : PeriodicEdge5 :=
1849  { base := periodicRelativeVertex5 row.base col.base, disp := col.disp }
1850
1851theorem periodicRelativeColumnOfOriginDisp5
1852    (rowDisp colDisp : Fin 7) (colBase : PeriodicVertex5) :
1853    periodicRelativeColumnOfRow5
1854        (periodicOriginEdgeOfDisp5 rowDisp)
1855        ({ base := colBase, disp := colDisp } : PeriodicEdge5) =
1856      ({ base := colBase, disp := colDisp } : PeriodicEdge5) := by
1857  simp [periodicRelativeColumnOfRow5, periodicOriginEdgeOfDisp5,
1858    periodicRelativeVertex5_origin_eq_self]
1859
1860/-- Endpoints of a relative-frame column are the relative-frame endpoints of the
1861global column. -/
1862theorem periodicRelativeColumnOfRow5_endpoints
1863    (row col : PeriodicEdge5) :
1864    (periodicRelativeColumnOfRow5 row col).endpoints =
1865      (periodicRelativeVertex5 row.base col.endpoints.1,
1866       periodicRelativeVertex5 row.base col.endpoints.2) := by
1867  rcases row with ⟨rowBase, rowDisp⟩
1868  rcases col with ⟨colBase, colDisp⟩
1869  rcases rowBase with ⟨rx, ryz⟩
1870  rcases ryz with ⟨ry, rz⟩
1871  rcases colBase with ⟨cx, cyz⟩
1872  rcases cyz with ⟨cy, cz⟩
1873  fin_cases colDisp <;>
1874    ext <;>
1875    simp [periodicRelativeColumnOfRow5, PeriodicEdge.endpoints,
1876      periodicRelativeVertex5, periodicSubFin5, addBits, dispBits, addBit, bit] <;>
1877    omega
1878
1879/-- Translating the endpoints of a relative-frame column back by the row base
1880recovers the endpoints of the original global column. -/
1881theorem periodicTranslateVertex5_relativeColumn_endpoints
1882    (row col : PeriodicEdge5) :
1883    (periodicTranslateVertex5 row.base
1884        (periodicRelativeColumnOfRow5 row col).endpoints.1,
1885      periodicTranslateVertex5 row.base
1886        (periodicRelativeColumnOfRow5 row col).endpoints.2) =
1887      col.endpoints := by
1888  rw [periodicRelativeColumnOfRow5_endpoints]
1889  simp [periodicTranslateVertex5_relative_eq_self]
1890
1891/-- First endpoint equality in a row-relative frame is equivalent to translated
1892global endpoint equality. -/
1893theorem periodicRelativeColumnOfRow5_endpoint_fst_eq_iff
1894    (row col : PeriodicEdge5) (v : PeriodicVertex5) :
1895    (periodicRelativeColumnOfRow5 row col).endpoints.1 = v ↔
1896      col.endpoints.1 = periodicTranslateVertex5 row.base v := by
1897  have hends := periodicTranslateVertex5_relativeColumn_endpoints row col
1898  have hfst :
1899      periodicTranslateVertex5 row.base
1900          (periodicRelativeColumnOfRow5 row col).endpoints.1 =
1901        col.endpoints.1 := congrArg Prod.fst hends
1902  constructor
1903  · intro h
1904    rw [← hfst, h]
1905  · intro h
1906    exact periodicTranslateVertex5_injective row.base (hfst.trans h)
1907
1908/-- Second endpoint equality in a row-relative frame is equivalent to translated
1909global endpoint equality. -/
1910theorem periodicRelativeColumnOfRow5_endpoint_snd_eq_iff
1911    (row col : PeriodicEdge5) (v : PeriodicVertex5) :
1912    (periodicRelativeColumnOfRow5 row col).endpoints.2 = v ↔
1913      col.endpoints.2 = periodicTranslateVertex5 row.base v := by
1914  have hends := periodicTranslateVertex5_relativeColumn_endpoints row col
1915  have hsnd :
1916      periodicTranslateVertex5 row.base
1917          (periodicRelativeColumnOfRow5 row col).endpoints.2 =
1918        col.endpoints.2 := congrArg Prod.snd hends
1919  constructor
1920  · intro h
1921    rw [← hsnd, h]
1922  · intro h
1923    exact periodicTranslateVertex5_injective row.base (hsnd.trans h)
1924
1925/-- Encoded first-endpoint equality in a row-relative frame is equivalent to
1926encoded shifted first-endpoint equality in the global frame. -/
1927theorem periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff
1928    (row col : PeriodicEdge5) (v : Fin PeriodicTorus5.K.nV) :
1929    periodicVertexEquiv5.symm
1930        (periodicRelativeColumnOfRow5 row col).endpoints.1 = v ↔
1931      periodicVertexEquiv5.symm col.endpoints.1 =
1932        periodicTranslateEncodedVertexIdx5 row.base v := by
1933  constructor
1934  · intro h
1935    apply periodicVertexEquiv5.injective
1936    simpa [periodicTranslateEncodedVertexIdx5] using
1937      (periodicRelativeColumnOfRow5_endpoint_fst_eq_iff row col
1938        (periodicVertexEquiv5 v)).1 (by
1939          simpa using congrArg periodicVertexEquiv5 h)
1940  · intro h
1941    have hglobal :
1942        col.endpoints.1 =
1943          periodicTranslateVertex5 row.base (periodicVertexEquiv5 v) := by
1944      simpa [periodicTranslateEncodedVertexIdx5] using
1945        congrArg periodicVertexEquiv5 h
1946    have hrel :=
1947      (periodicRelativeColumnOfRow5_endpoint_fst_eq_iff row col
1948        (periodicVertexEquiv5 v)).2 hglobal
1949    simpa using congrArg periodicVertexEquiv5.symm hrel
1950
1951/-- Encoded second-endpoint equality in a row-relative frame is equivalent to
1952encoded shifted second-endpoint equality in the global frame. -/
1953theorem periodicRelativeColumnOfRow5_encoded_endpoint_snd_eq_iff
1954    (row col : PeriodicEdge5) (v : Fin PeriodicTorus5.K.nV) :
1955    periodicVertexEquiv5.symm
1956        (periodicRelativeColumnOfRow5 row col).endpoints.2 = v ↔
1957      periodicVertexEquiv5.symm col.endpoints.2 =
1958        periodicTranslateEncodedVertexIdx5 row.base v := by
1959  constructor
1960  · intro h
1961    apply periodicVertexEquiv5.injective
1962    simpa [periodicTranslateEncodedVertexIdx5] using
1963      (periodicRelativeColumnOfRow5_endpoint_snd_eq_iff row col
1964        (periodicVertexEquiv5 v)).1 (by
1965          simpa using congrArg periodicVertexEquiv5 h)
1966  · intro h
1967    have hglobal :
1968        col.endpoints.2 =
1969          periodicTranslateVertex5 row.base (periodicVertexEquiv5 v) := by
1970      simpa [periodicTranslateEncodedVertexIdx5] using
1971        congrArg periodicVertexEquiv5 h
1972    have hrel :=
1973      (periodicRelativeColumnOfRow5_endpoint_snd_eq_iff row col
1974        (periodicVertexEquiv5 v)).2 hglobal
1975    simpa using congrArg periodicVertexEquiv5.symm hrel
1976
1977/-- A row-frame translate of one conformal generator column is exactly the
1978globally shifted conformal generator column. -/
1979theorem periodicConformalGenerator5_relativeColumn_eq_shift
1980    (row col : PeriodicEdge5) (v : Fin PeriodicTorus5.K.nV) :
1981    periodicConformalGenerator5 v
1982        (periodicRelativeColumnOfRow5 row col) =
1983      periodicConformalGenerator5
1984        (periodicTranslateEncodedVertexIdx5 row.base v) col := by
1985  rw [periodicConformalGenerator5_apply_endpoint,
1986    periodicConformalGenerator5_apply_endpoint]
1987  simp [periodicRelativeColumnOfRow5_encoded_endpoint_fst_eq_iff,
1988    periodicRelativeColumnOfRow5_encoded_endpoint_snd_eq_iff]
1989
1990/-- A row-frame translate of one longitudinal gauge generator column is exactly
1991the globally shifted longitudinal gauge generator column. -/
1992theorem periodicLongitudinalGaugeGenerator5_relativeColumn_eq_shift
1993    (row col : PeriodicEdge5) (idx : PeriodicLongitudinalGaugeIdx5) :
1994    periodicLongitudinalGaugeGenerator5 idx
1995        (periodicRelativeColumnOfRow5 row col) =
1996      periodicLongitudinalGaugeGenerator5
1997        (periodicTranslateLongitudinalGaugeIdx5 row.base idx) col := by
1998  rcases idx with ⟨idxVertex, idxComponent⟩
1999  have hdisp : (periodicRelativeColumnOfRow5 row col).disp = col.disp := rfl
2000  simp [periodicLongitudinalGaugeGenerator5,
2001    periodicTranslateLongitudinalGaugeIdx5,
2002    hdisp,
2003    periodicRelativeColumnOfRow5_endpoint_fst_eq_iff,
2004    periodicRelativeColumnOfRow5_endpoint_snd_eq_iff]
2005
2006/-- A row-frame translate of any combined normal-equation generator column is
2007exactly the globally shifted combined generator column. -/
2008theorem periodicTTNormalEquationGenerator5_relativeColumn_eq_shift
2009    (row col : PeriodicEdge5) (idx : PeriodicTTNormalEquationIdx5) :
2010    periodicTTNormalEquationGenerator5 idx
2011        (periodicRelativeColumnOfRow5 row col) =
2012      periodicTTNormalEquationGenerator5
2013        (periodicTranslateTTNormalEquationIdx5 row.base idx) col := by
2014  cases idx with
2015  | inl v =>
2016      exact periodicConformalGenerator5_relativeColumn_eq_shift row col v
2017  | inr i =>
2018      exact periodicLongitudinalGaugeGenerator5_relativeColumn_eq_shift row col i
2019
2020/-- Encoded vertex-index translation by a row base, packaged as an equivalence. -/
2021noncomputable def periodicTranslateEncodedVertexIdxEquiv5
2022    (base : PeriodicVertex5) :
2023    Fin PeriodicTorus5.K.nV ≃ Fin PeriodicTorus5.K.nV where
2024  toFun := periodicTranslateEncodedVertexIdx5 base
2025  invFun := fun v =>
2026    periodicVertexEquiv5.symm
2027      (periodicRelativeVertex5 base (periodicVertexEquiv5 v))
2028  left_inv := by
2029    intro v
2030    apply periodicVertexEquiv5.injective
2031    simp [periodicTranslateEncodedVertexIdx5,
2032      periodicRelativeVertex5_translate_eq_self]
2033  right_inv := by
2034    intro v
2035    apply periodicVertexEquiv5.injective
2036    simp [periodicTranslateEncodedVertexIdx5,
2037      periodicTranslateVertex5_relative_eq_self]
2038
2039/-- Longitudinal gauge-index translation by a row base, packaged as an equivalence. -/
2040def periodicTranslateLongitudinalGaugeIdxEquiv5
2041    (base : PeriodicVertex5) :
2042    PeriodicLongitudinalGaugeIdx5 ≃ PeriodicLongitudinalGaugeIdx5 where
2043  toFun := periodicTranslateLongitudinalGaugeIdx5 base
2044  invFun := fun idx => (periodicRelativeVertex5 base idx.1, idx.2)
2045  left_inv := by
2046    intro idx
2047    rcases idx with ⟨v, j⟩
2048    simp [periodicTranslateLongitudinalGaugeIdx5,
2049      periodicRelativeVertex5_translate_eq_self]
2050  right_inv := by
2051    intro idx
2052    rcases idx with ⟨v, j⟩
2053    simp [periodicTranslateLongitudinalGaugeIdx5,
2054      periodicTranslateVertex5_relative_eq_self]
2055
2056/-- Combined normal-equation index translation by a row base, packaged as an
2057equivalence. -/
2058noncomputable def periodicTranslateTTNormalEquationIdxEquiv5
2059    (base : PeriodicVertex5) :
2060    PeriodicTTNormalEquationIdx5 ≃ PeriodicTTNormalEquationIdx5 where
2061  toFun := periodicTranslateTTNormalEquationIdx5 base
2062  invFun
2063    | Sum.inl v => Sum.inl ((periodicTranslateEncodedVertexIdxEquiv5 base).symm v)
2064    | Sum.inr i => Sum.inr ((periodicTranslateLongitudinalGaugeIdxEquiv5 base).symm i)
2065  left_inv := by
2066    intro idx
2067    cases idx with
2068    | inl v =>
2069        simp only [periodicTranslateTTNormalEquationIdx5]
2070        exact congrArg Sum.inl
2071          ((periodicTranslateEncodedVertexIdxEquiv5 base).left_inv v)
2072    | inr i =>
2073        simp only [periodicTranslateTTNormalEquationIdx5]
2074        exact congrArg Sum.inr
2075          ((periodicTranslateLongitudinalGaugeIdxEquiv5 base).left_inv i)
2076  right_inv := by
2077    intro idx
2078    cases idx with
2079    | inl v =>
2080        simp only [periodicTranslateTTNormalEquationIdx5]
2081        exact congrArg Sum.inl
2082          ((periodicTranslateEncodedVertexIdxEquiv5 base).right_inv v)
2083    | inr i =>
2084        simp only [periodicTranslateTTNormalEquationIdx5]
2085        exact congrArg Sum.inr
2086          ((periodicTranslateLongitudinalGaugeIdxEquiv5 base).right_inv i)
2087
2088/-- Combined generator map viewed in the coordinate frame of a row edge. -/
2089def periodicRelativeTTNormalEquationGeneratorMap5
2090    (row : PeriodicEdge5) (coeff : PeriodicTTNormalEquationIdx5 → ℝ) :
2091    PeriodicEdgePerturbation5 :=
2092  fun col => periodicTTNormalEquationGeneratorMap5 coeff
2093    (periodicRelativeColumnOfRow5 row col)
2094
2095/-- Relative-frame combined generator maps are global generator maps with the
2096coefficient vector reindexed by the row-base translation equivalence. -/
2097theorem periodicRelativeTTNormalEquationGeneratorMap5_eq_shiftedMap
2098    (row : PeriodicEdge5) (coeff : PeriodicTTNormalEquationIdx5 → ℝ)
2099    (col : PeriodicEdge5) :
2100    periodicRelativeTTNormalEquationGeneratorMap5 row coeff col =
2101      periodicTTNormalEquationGeneratorMap5
2102        (fun idx => coeff ((periodicTranslateTTNormalEquationIdxEquiv5 row.base).symm idx))
2103        col := by
2104  classical
2105  let σ := periodicTranslateTTNormalEquationIdxEquiv5 row.base
2106  unfold periodicRelativeTTNormalEquationGeneratorMap5
2107    periodicTTNormalEquationGeneratorMap5 periodicGaugeGeneratorMap5
2108  calc
2109    (∑ idx : PeriodicTTNormalEquationIdx5,
2110        coeff idx *
2111          periodicTTNormalEquationGenerator5 idx
2112            (periodicRelativeColumnOfRow5 row col)) =
2113      ∑ idx : PeriodicTTNormalEquationIdx5,
2114        coeff idx *
2115          periodicTTNormalEquationGenerator5 (σ idx) col := by
2116        refine Finset.sum_congr rfl ?_
2117        intro idx _
2118        rw [periodicTTNormalEquationGenerator5_relativeColumn_eq_shift]
2119        rfl
2120    _ =
2121      ∑ idx : PeriodicTTNormalEquationIdx5,
2122        coeff (σ.symm idx) *
2123          periodicTTNormalEquationGenerator5 idx col := by
2124        exact Fintype.sum_equiv σ
2125          (fun idx : PeriodicTTNormalEquationIdx5 =>
2126            coeff idx * periodicTTNormalEquationGenerator5 (σ idx) col)
2127          (fun idx : PeriodicTTNormalEquationIdx5 =>
2128            coeff (σ.symm idx) * periodicTTNormalEquationGenerator5 idx col)
2129          (fun idx => by simp [σ])
2130
2131/-- Missing shifted-generator lemma for the relative-frame route: every TT
2132perturbation is orthogonal to every row-frame translate of the combined
2133conformal/longitudinal generator map. -/
2134def PeriodicRelativeTTGeneratorOrthogonalOnTT5 : Prop :=
2135  ∀ ε,
2136    PeriodicLongitudinalTTSubspace5 ε →
2137      ∀ (row : PeriodicEdge5) (coeff : PeriodicTTNormalEquationIdx5 → ℝ),
2138        periodicEdgeInnerProduct5 ε
2139          (periodicRelativeTTNormalEquationGeneratorMap5 row coeff) = 0
2140
2141/-- Closure target behind shifted-generator orthogonality: every row-frame
2142translate of a combined normal-equation generator must split back into the
2143fixed conformal and longitudinal-gauge images. -/
2144def PeriodicRelativeTTGeneratorClosure5 : Prop :=
2145  ∀ (row : PeriodicEdge5) (coeff : PeriodicTTNormalEquationIdx5 → ℝ),
2146    ∃ (conformalCoeff : Fin PeriodicTorus5.K.nV → ℝ)
2147      (gaugeCoeff : PeriodicLongitudinalGaugeIdx5 → ℝ),
2148      ∀ col,
2149        periodicRelativeTTNormalEquationGeneratorMap5 row coeff col =
2150          periodicConformalGeneratorMap5 conformalCoeff col +
2151            periodicLongitudinalGaugeMap5 gaugeCoeff col
2152
2153/-- The row-frame translated combined generator space is exactly closed inside
2154the fixed conformal plus longitudinal-gauge image. -/
2155theorem periodicRelativeTTGeneratorClosure5_holds :
2156    PeriodicRelativeTTGeneratorClosure5 := by
2157  classical
2158  intro row coeff
2159  let shiftedCoeff : PeriodicTTNormalEquationIdx5 → ℝ :=
2160    fun idx => coeff ((periodicTranslateTTNormalEquationIdxEquiv5 row.base).symm idx)
2161  refine ⟨
2162    periodicTTNormalEquationConformalCoeff5 shiftedCoeff,
2163    periodicTTNormalEquationGaugeCoeff5 shiftedCoeff,
2164    ?_⟩
2165  intro col
2166  rw [periodicRelativeTTNormalEquationGeneratorMap5_eq_shiftedMap]
2167  exact periodicTTNormalEquationGeneratorMap5_eq_split shiftedCoeff col
2168
2169/-- Closure of row-frame generator translates into the fixed conformal/gauge
2170images proves the shifted-generator orthogonality lemma. -/
2171theorem PeriodicRelativeTTGeneratorOrthogonalOnTT5.ofClosure
2172    (hclosure : PeriodicRelativeTTGeneratorClosure5) :
2173    PeriodicRelativeTTGeneratorOrthogonalOnTT5 := by
2174  intro ε hε row coeff
2175  rcases hclosure row coeff with ⟨conformalCoeff, gaugeCoeff, hsplit⟩
2176  have hfun :
2177      periodicRelativeTTNormalEquationGeneratorMap5 row coeff =
2178        fun col =>
2179          periodicConformalGeneratorMap5 conformalCoeff col +
2180            periodicLongitudinalGaugeMap5 gaugeCoeff col := by
2181    funext col
2182    exact hsplit col
2183  have hc :
2184      periodicEdgeInnerProduct5 ε
2185        (periodicConformalGeneratorMap5 conformalCoeff) = 0 :=
2186    hε.1 (periodicConformalGeneratorMap5 conformalCoeff)
2187      (periodicConformalGeneratorMap5_mem conformalCoeff)
2188  have hg :
2189      periodicEdgeInnerProduct5 ε
2190        (periodicLongitudinalGaugeMap5 gaugeCoeff) = 0 :=
2191    hε.2 (periodicLongitudinalGaugeMap5 gaugeCoeff) ⟨gaugeCoeff, rfl⟩
2192  rw [hfun, periodicEdgeInnerProduct5_add_right, hc, hg, add_zero]
2193
2194/-- Encoded edge index for the origin-row representative of a displacement. -/
2195def encodedOriginEdgeOfDisp5 (disp : Fin 7) : Fin PeriodicTorus5.K.nE :=
2196  PeriodicTorus5.edgeEquiv.symm (periodicOriginEdgeOfDisp5 disp)
2197
2198theorem encodedOriginEdgeOfDisp5_equiv
2199    (disp : Fin 7) :
2200    PeriodicTorus5.edgeEquiv (encodedOriginEdgeOfDisp5 disp) =
2201      periodicOriginEdgeOfDisp5 disp := by
2202  simp [encodedOriginEdgeOfDisp5]
2203
2204/-- Apply a finite edge-kernel operator to an edge perturbation. -/
2205def periodicEdgeKernelOperator5
2206    (kernel : PeriodicEdgeOperatorKernel5)
2207    (ε : PeriodicEdgePerturbation5) : PeriodicEdgePerturbation5 :=
2208  fun e => ∑ f : PeriodicEdge5, kernel e f * ε f
2209
2210/-- Row of a finite edge-kernel operator as an edge perturbation. -/
2211def periodicEdgeKernelRowVector5
2212    (kernel : PeriodicEdgeOperatorKernel5)
2213    (e : PeriodicEdge5) : PeriodicEdgePerturbation5 :=
2214  fun f => kernel e f
2215
2216/-- Kernel-operator evaluation is pairing against the corresponding row vector,
2217up to the symmetry of real multiplication. -/
2218theorem periodicEdgeKernelOperator5_eq_inner_row
2219    (kernel : PeriodicEdgeOperatorKernel5)
2220    (ε : PeriodicEdgePerturbation5)
2221    (e : PeriodicEdge5) :
2222    periodicEdgeKernelOperator5 kernel ε e =
2223      periodicEdgeInnerProduct5 ε (periodicEdgeKernelRowVector5 kernel e) := by
2224  unfold periodicEdgeKernelOperator5 periodicEdgeInnerProduct5 periodicEdgeKernelRowVector5
2225  refine Finset.sum_congr rfl ?_
2226  intro f _
2227  ring
2228
2229/-- Rowwise agreement of edge-kernel operators on a TT perturbation gives
2230pointwise agreement of the resulting edge perturbations. -/
2231theorem periodicEdgeKernelOperator5_eq_of_row_eq
2232    (reggeKernel lichnerowiczKernel : PeriodicEdgeOperatorKernel5)
2233    (ε : PeriodicEdgePerturbation5)
2234    (hrow :
2235      ∀ e : PeriodicEdge5,
2236        periodicEdgeKernelOperator5 reggeKernel ε e =
2237          periodicEdgeKernelOperator5 lichnerowiczKernel ε e) :
2238    periodicEdgeKernelOperator5 reggeKernel ε =
2239      periodicEdgeKernelOperator5 lichnerowiczKernel ε := by
2240  funext e
2241  exact hrow e
2242
2243/-- Entrywise equality of two finite edge kernels gives equality of their
2244operators on every edge perturbation. -/
2245theorem periodicEdgeKernelOperator5_eq_of_kernel_eq
2246    (reggeKernel lichnerowiczKernel : PeriodicEdgeOperatorKernel5)
2247    (hkernel : ∀ e f : PeriodicEdge5, reggeKernel e f = lichnerowiczKernel e f)
2248    (ε : PeriodicEdgePerturbation5) :
2249    periodicEdgeKernelOperator5 reggeKernel ε =
2250      periodicEdgeKernelOperator5 lichnerowiczKernel ε := by
2251  apply periodicEdgeKernelOperator5_eq_of_row_eq
2252  intro e
2253  unfold periodicEdgeKernelOperator5
2254  refine Finset.sum_congr rfl ?_
2255  intro f _
2256  rw [hkernel e f]
2257
2258/-- Difference kernel between the Regge TT Hessian stencil and the lattice
2259Lichnerowicz stencil. -/
2260def periodicEdgeKernelResidual5
2261    (reggeKernel lichnerowiczKernel : PeriodicEdgeOperatorKernel5) :
2262    PeriodicEdgeOperatorKernel5 :=
2263  fun e f => reggeKernel e f - lichnerowiczKernel e f
2264
2265/-- Applying the residual kernel is the difference of the two kernel operators. -/
2266theorem periodicEdgeKernelOperator5_residual_eq_sub
2267    (reggeKernel lichnerowiczKernel : PeriodicEdgeOperatorKernel5)
2268    (ε : PeriodicEdgePerturbation5)
2269    (e : PeriodicEdge5) :
2270    periodicEdgeKernelOperator5
2271      (periodicEdgeKernelResidual5 reggeKernel lichnerowiczKernel) ε e =
2272      periodicEdgeKernelOperator5 reggeKernel ε e -
2273        periodicEdgeKernelOperator5 lichnerowiczKernel ε e := by
2274  unfold periodicEdgeKernelOperator5 periodicEdgeKernelResidual5
2275  calc
2276    (∑ f : PeriodicEdge5, (reggeKernel e f - lichnerowiczKernel e f) * ε f)
2277        =
2278        ∑ f : PeriodicEdge5,
2279          (reggeKernel e f * ε f - lichnerowiczKernel e f * ε f) := by
2280          refine Finset.sum_congr rfl ?_
2281          intro f _
2282          ring
2283    _ =
2284        (∑ f : PeriodicEdge5, reggeKernel e f * ε f) -
2285          ∑ f : PeriodicEdge5, lichnerowiczKernel e f * ε f := by
2286          rw [Finset.sum_sub_distrib]
2287
2288/-- The exact forward Track 1.D Hessian/Lichnerowicz target at `N = 5`: on TT
2289edge perturbations, the Regge Hessian operator agrees with the lattice
2290Lichnerowicz operator. -/
2291def PeriodicTTHessianMatchesLichnerowiczAtN5
2292    (reggeHessianTT latticeLichnerowiczTT :
2293      PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5) : Prop :=
2294  ∀ ε,
2295    PeriodicLongitudinalTTSubspace5 ε →
2296      reggeHessianTT ε = latticeLichnerowiczTT ε
2297
2298/-- Data object for the TT Hessian-to-Lichnerowicz operator match.  The actual
2299analytic work is to instantiate the two operators from the Regge Hessian and the
2300discrete spin-2 Lichnerowicz stencil, then prove `matches_on_tt`. -/
2301structure PeriodicTTHessianLichnerowiczMatchData5 where
2302  reggeHessianTT :
2303    PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
2304  latticeLichnerowiczTT :
2305    PeriodicEdgePerturbation5 → PeriodicEdgePerturbation5
2306  matches_on_tt :
2307    PeriodicTTHessianMatchesLichnerowiczAtN5
2308      reggeHessianTT latticeLichnerowiczTT
2309
2310/-- Rowwise kernel data for proving the TT Hessian-to-Lichnerowicz operator
2311match.  The intended physical closure is to instantiate `reggeHessianKernel`
2312from the Regge second-variation edge Hessian and `latticeLichnerowiczKernel`
2313from the spin-2 lattice stencil, then prove `kernel_rows_match_on_tt`. -/
2314structure PeriodicTTHessianLichnerowiczKernelRowData5 where
2315  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2316  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2317  kernel_rows_match_on_tt :
2318    ∀ ε,
2319      PeriodicLongitudinalTTSubspace5 ε →
2320        ∀ e : PeriodicEdge5,
2321          periodicEdgeKernelOperator5 reggeHessianKernel ε e =
2322            periodicEdgeKernelOperator5 latticeLichnerowiczKernel ε e
2323
2324/-- Entrywise kernel data is a stronger, stencil-level route to the same TT
2325Hessian-to-Lichnerowicz operator match. -/
2326structure PeriodicTTHessianLichnerowiczKernelEntryData5 where
2327  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2328  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2329  kernel_entries_match :
2330    ∀ e f : PeriodicEdge5,
2331      reggeHessianKernel e f = latticeLichnerowiczKernel e f
2332
2333/-- Residual-kernel vanishing on TT perturbations is the most compact finite
2334calculation target for the TT Hessian-to-Lichnerowicz comparison. -/
2335structure PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 where
2336  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2337  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2338  residual_zero_on_tt :
2339    ∀ ε,
2340      PeriodicLongitudinalTTSubspace5 ε →
2341        periodicEdgeKernelOperator5
2342          (periodicEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel)
2343          ε = fun _ => 0
2344
2345/-- Row-span data for the residual kernel: every residual row belongs to the
2346combined conformal plus longitudinal generator span.  This is the sharp finite
2347stencil target for the TT Hessian/Lichnerowicz comparison. -/
2348structure PeriodicTTHessianLichnerowiczResidualRowSpanData5 where
2349  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2350  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2351  residual_row_mem_generator_span :
2352    ∀ e : PeriodicEdge5,
2353      ∃ coeff : PeriodicTTNormalEquationIdx5 → ℝ,
2354        periodicEdgeKernelRowVector5
2355          (periodicEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel) e =
2356          periodicTTNormalEquationGeneratorMap5 coeff
2357
2358/-- Explicit coefficient form of the residual-row span target.  This is the
2359finite table the remaining TT stencil calculation should produce: for each
2360edge-row, a combined conformal/longitudinal coefficient vector whose generator
2361map is exactly the residual row. -/
2362structure PeriodicTTHessianLichnerowiczResidualRowCoeffData5 where
2363  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2364  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2365  residualRowCoeff :
2366    PeriodicEdge5 → PeriodicTTNormalEquationIdx5 → ℝ
2367  residual_row_eq_generatorMap :
2368    ∀ e : PeriodicEdge5,
2369      periodicEdgeKernelRowVector5
2370        (periodicEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel) e =
2371        periodicTTNormalEquationGeneratorMap5 (residualRowCoeff e)
2372
2373/-- Entrywise version of the explicit residual-row coefficient target.  This is
2374the certificate-friendly scalar form: every residual kernel entry equals the
2375corresponding entry of the row's generator-map reconstruction. -/
2376structure PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5 where
2377  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2378  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2379  residualRowCoeff :
2380    PeriodicEdge5 → PeriodicTTNormalEquationIdx5 → ℝ
2381  residual_entry_eq_generatorMap :
2382    ∀ e f : PeriodicEdge5,
2383      periodicEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f =
2384        periodicTTNormalEquationGeneratorMap5 (residualRowCoeff e) f
2385
2386/-- Raw scalar formula form of the residual-row coefficient target.  This is the
2387unwrapped finite identity: Regge kernel entry minus Lichnerowicz kernel entry
2388equals the generator-map reconstruction entry. -/
2389structure PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 where
2390  reggeHessianKernel : PeriodicEdgeOperatorKernel5
2391  latticeLichnerowiczKernel : PeriodicEdgeOperatorKernel5
2392  residualRowCoeff :
2393    PeriodicEdge5 → PeriodicTTNormalEquationIdx5 → ℝ
2394  residual_entry_formula :
2395    ∀ e f : PeriodicEdge5,
2396      reggeHessianKernel e f - latticeLichnerowiczKernel e f =
2397        periodicTTNormalEquationGeneratorMap5 (residualRowCoeff e) f
2398
2399/-- Encoded finite-index form of the raw scalar TT residual formula.  This is
2400the certificate surface for kernels produced over the encoded `Fin K.nE` edge
2401indexing of the canonical `N = 5` periodic Freudenthal torus. -/
2402structure EncodedTTHessianLichnerowiczResidualEntryFormulaData5 where
2403  reggeHessianKernel : EncodedEdgeOperatorKernel5
2404  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2405  residualRowCoeff :
2406    PeriodicEdge5 → PeriodicTTNormalEquationIdx5 → ℝ
2407  encoded_residual_entry_formula :
2408    ∀ e f : Fin PeriodicTorus5.K.nE,
2409      reggeHessianKernel e f - latticeLichnerowiczKernel e f =
2410        periodicTTNormalEquationGeneratorMap5
2411          (residualRowCoeff (PeriodicTorus5.edgeEquiv e))
2412          (PeriodicTorus5.edgeEquiv f)
2413
2414/-- Encoded residual-kernel certificate form.  This lets the finite calculation
2415emit the already-subtracted residual matrix, prove it is `Regge - Lichnerowicz`,
2416and then compare that residual directly to the generator-map reconstruction. -/
2417structure EncodedTTHessianLichnerowiczResidualKernelFormulaData5 where
2418  reggeHessianKernel : EncodedEdgeOperatorKernel5
2419  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2420  residualKernel : EncodedEdgeOperatorKernel5
2421  residualRowCoeff :
2422    PeriodicEdge5 → PeriodicTTNormalEquationIdx5 → ℝ
2423  residualKernel_eq_sub :
2424    ∀ e f : Fin PeriodicTorus5.K.nE,
2425      residualKernel e f =
2426        encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f
2427  residualKernel_entry_formula :
2428    ∀ e f : Fin PeriodicTorus5.K.nE,
2429      residualKernel e f =
2430        periodicTTNormalEquationGeneratorMap5
2431          (residualRowCoeff (PeriodicTorus5.edgeEquiv e))
2432          (PeriodicTorus5.edgeEquiv f)
2433
2434/-- Displacement-row form of the encoded residual-kernel certificate.  Translation
2435normalizes every encoded row to the origin edge with the same displacement, so
2436the finite table only has seven row families. -/
2437structure EncodedTTHessianLichnerowiczResidualDispRowFormulaData5 where
2438  reggeHessianKernel : EncodedEdgeOperatorKernel5
2439  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2440  residualKernel : EncodedEdgeOperatorKernel5
2441  residualDispCoeff :
2442    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2443  residualKernel_eq_sub :
2444    ∀ e f : Fin PeriodicTorus5.K.nE,
2445      residualKernel e f =
2446        encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f
2447  residualKernel_row_translation :
2448    ∀ e f : Fin PeriodicTorus5.K.nE,
2449      residualKernel e f =
2450        residualKernel
2451          (encodedOriginEdgeOfDisp5 (PeriodicTorus5.edgeEquiv e).disp) f
2452  residual_origin_row_formula :
2453    ∀ (disp : Fin 7) (f : Fin PeriodicTorus5.K.nE),
2454      residualKernel (encodedOriginEdgeOfDisp5 disp) f =
2455        periodicTTNormalEquationGeneratorMap5
2456          (residualDispCoeff disp)
2457          (PeriodicTorus5.edgeEquiv f)
2458
2459/-- Seven-row table form of the encoded residual certificate.  The generator can
2460emit only the origin residual rows, then separately prove that every matrix row
2461translates to the appropriate row of this table. -/
2462structure EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5 where
2463  reggeHessianKernel : EncodedEdgeOperatorKernel5
2464  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2465  residualKernel : EncodedEdgeOperatorKernel5
2466  residualOriginRow :
2467    Fin 7 → Fin PeriodicTorus5.K.nE → ℝ
2468  residualDispCoeff :
2469    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2470  residualKernel_eq_sub :
2471    ∀ e f : Fin PeriodicTorus5.K.nE,
2472      residualKernel e f =
2473        encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f
2474  residualOriginRow_eq_origin :
2475    ∀ (disp : Fin 7) (f : Fin PeriodicTorus5.K.nE),
2476      residualOriginRow disp f =
2477        residualKernel (encodedOriginEdgeOfDisp5 disp) f
2478  residualKernel_row_translation :
2479    ∀ e f : Fin PeriodicTorus5.K.nE,
2480      residualKernel e f =
2481        residualOriginRow (PeriodicTorus5.edgeEquiv e).disp f
2482  residualOriginRow_entry_formula :
2483    ∀ (disp : Fin 7) (f : Fin PeriodicTorus5.K.nE),
2484      residualOriginRow disp f =
2485        periodicTTNormalEquationGeneratorMap5
2486          (residualDispCoeff disp)
2487          (PeriodicTorus5.edgeEquiv f)
2488
2489/-- Typed-column table form of the seven origin-row residual certificate.  This
2490is the generator-facing surface: each table entry is indexed by the origin-row
2491displacement, the column base vertex, and the column displacement. -/
2492structure EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5 where
2493  reggeHessianKernel : EncodedEdgeOperatorKernel5
2494  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2495  residualKernel : EncodedEdgeOperatorKernel5
2496  residualOriginColumn :
2497    Fin 7 → PeriodicVertex5 → Fin 7 → ℝ
2498  residualDispCoeff :
2499    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2500  residualKernel_eq_sub :
2501    ∀ e f : Fin PeriodicTorus5.K.nE,
2502      residualKernel e f =
2503        encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f
2504  residualOriginColumn_eq_origin :
2505    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2506      residualOriginColumn rowDisp colBase colDisp =
2507        residualKernel
2508          (encodedOriginEdgeOfDisp5 rowDisp)
2509          (PeriodicTorus5.edgeEquiv.symm
2510            ({ base := colBase, disp := colDisp } : PeriodicEdge5))
2511  residualKernel_row_translation :
2512    ∀ e f : Fin PeriodicTorus5.K.nE,
2513      residualKernel e f =
2514        residualOriginColumn
2515          (PeriodicTorus5.edgeEquiv e).disp
2516          (PeriodicTorus5.edgeEquiv f).base
2517          (PeriodicTorus5.edgeEquiv f).disp
2518  residualOriginColumn_entry_formula :
2519    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2520      residualOriginColumn rowDisp colBase colDisp =
2521        periodicTTNormalEquationGeneratorMap5
2522          (residualDispCoeff rowDisp)
2523          ({ base := colBase, disp := colDisp } : PeriodicEdge5)
2524
2525/-- Raw typed-column residual certificate.  This removes the explicit residual
2526matrix from the generator-facing input: the finite calculation supplies only the
2527origin-column residual table and a translation law for the encoded
2528`Regge - Lichnerowicz` residual. -/
2529structure EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5 where
2530  reggeHessianKernel : EncodedEdgeOperatorKernel5
2531  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2532  residualOriginColumn :
2533    Fin 7 → PeriodicVertex5 → Fin 7 → ℝ
2534  residualDispCoeff :
2535    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2536  residualOriginColumn_eq_sub :
2537    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2538      residualOriginColumn rowDisp colBase colDisp =
2539        reggeHessianKernel
2540          (encodedOriginEdgeOfDisp5 rowDisp)
2541          (PeriodicTorus5.edgeEquiv.symm
2542            ({ base := colBase, disp := colDisp } : PeriodicEdge5)) -
2543        latticeLichnerowiczKernel
2544          (encodedOriginEdgeOfDisp5 rowDisp)
2545          (PeriodicTorus5.edgeEquiv.symm
2546            ({ base := colBase, disp := colDisp } : PeriodicEdge5))
2547  encodedResidual_row_translation :
2548    ∀ e f : Fin PeriodicTorus5.K.nE,
2549      encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f =
2550        residualOriginColumn
2551          (PeriodicTorus5.edgeEquiv e).disp
2552          (PeriodicTorus5.edgeEquiv f).base
2553          (PeriodicTorus5.edgeEquiv f).disp
2554  residualOriginColumn_entry_formula :
2555    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2556      residualOriginColumn rowDisp colBase colDisp =
2557        periodicTTNormalEquationGeneratorMap5
2558          (residualDispCoeff rowDisp)
2559          ({ base := colBase, disp := colDisp } : PeriodicEdge5)
2560
2561/-- Coefficient-only origin-column formula data for the TT
2562Hessian/Lichnerowicz residual.  This is the smallest generator-facing surface:
2563it stores the two kernels and the seven residual-generator coefficient rows,
2564then proves the origin-row scalar formulas and the translated residual formula
2565directly against the generator map. -/
2566structure EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5 where
2567  reggeHessianKernel : EncodedEdgeOperatorKernel5
2568  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2569  residualDispCoeff :
2570    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2571  originColumn_entry_formula :
2572    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2573      reggeHessianKernel
2574          (encodedOriginEdgeOfDisp5 rowDisp)
2575          (PeriodicTorus5.edgeEquiv.symm
2576            ({ base := colBase, disp := colDisp } : PeriodicEdge5)) -
2577        latticeLichnerowiczKernel
2578          (encodedOriginEdgeOfDisp5 rowDisp)
2579          (PeriodicTorus5.edgeEquiv.symm
2580            ({ base := colBase, disp := colDisp } : PeriodicEdge5)) =
2581        periodicTTNormalEquationGeneratorMap5
2582          (residualDispCoeff rowDisp)
2583          ({ base := colBase, disp := colDisp } : PeriodicEdge5)
2584  encodedResidual_entry_formula :
2585    ∀ e f : Fin PeriodicTorus5.K.nE,
2586      encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f =
2587        periodicTTNormalEquationGeneratorMap5
2588          (residualDispCoeff (PeriodicTorus5.edgeEquiv e).disp)
2589          (PeriodicTorus5.edgeEquiv f)
2590
2591/-- Coefficient-only translated residual formula data for the TT
2592Hessian/Lichnerowicz residual.  This is a smaller certificate surface than
2593`EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5`: once the translated
2594residual formula is known, the origin-column scalar formula follows by
2595specializing the row to the origin edge. -/
2596structure EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5 where
2597  reggeHessianKernel : EncodedEdgeOperatorKernel5
2598  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2599  residualDispCoeff :
2600    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2601  encodedResidual_entry_formula :
2602    ∀ e f : Fin PeriodicTorus5.K.nE,
2603      encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f =
2604        periodicTTNormalEquationGeneratorMap5
2605          (residualDispCoeff (PeriodicTorus5.edgeEquiv e).disp)
2606          (PeriodicTorus5.edgeEquiv f)
2607
2608/-- Origin-column formula data for a relative-frame translated residual
2609certificate.  This records the part of the relative certificate that agrees with
2610the existing origin-row generator map, without asserting the absolute translated
2611formula for every row. -/
2612structure EncodedTTHessianLichnerowiczCoeffRelativeOriginColumnFormulaData5 where
2613  reggeHessianKernel : EncodedEdgeOperatorKernel5
2614  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2615  residualDispCoeff :
2616    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2617  originColumn_entry_formula :
2618    ∀ (rowDisp : Fin 7) (colBase : PeriodicVertex5) (colDisp : Fin 7),
2619      reggeHessianKernel
2620          (encodedOriginEdgeOfDisp5 rowDisp)
2621          (PeriodicTorus5.edgeEquiv.symm
2622            ({ base := colBase, disp := colDisp } : PeriodicEdge5)) -
2623        latticeLichnerowiczKernel
2624          (encodedOriginEdgeOfDisp5 rowDisp)
2625          (PeriodicTorus5.edgeEquiv.symm
2626            ({ base := colBase, disp := colDisp } : PeriodicEdge5)) =
2627        periodicTTNormalEquationGeneratorMap5
2628          (residualDispCoeff rowDisp)
2629          ({ base := colBase, disp := colDisp } : PeriodicEdge5)
2630
2631/-- Relative-frame coefficient-only translated residual formula data.  Generated
2632physical stencils are translation-covariant after each row is re-based at its
2633own edge base.  This diagnostic surface records that fact separately from the
2634stronger absolute translated certificate above. -/
2635structure EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5 where
2636  reggeHessianKernel : EncodedEdgeOperatorKernel5
2637  latticeLichnerowiczKernel : EncodedEdgeOperatorKernel5
2638  residualDispCoeff :
2639    Fin 7 → PeriodicTTNormalEquationIdx5 → ℝ
2640  encodedResidual_relative_entry_formula :
2641    ∀ e f : Fin PeriodicTorus5.K.nE,
2642      encodedEdgeKernelResidual5 reggeHessianKernel latticeLichnerowiczKernel e f =
2643        periodicTTNormalEquationGeneratorMap5
2644          (residualDispCoeff (PeriodicTorus5.edgeEquiv e).disp)
2645          (periodicRelativeColumnOfRow5
2646            (PeriodicTorus5.edgeEquiv e)
2647            (PeriodicTorus5.edgeEquiv f))
2648
2649/-- Relative-frame translated data plus the shifted-generator orthogonality
2650lemma is enough to prove the residual kernel vanishes on TT perturbations.
2651The separate orthogonality field is the exact mathematical gap left by the
2652Regge Schläfli candidate diagnostics. -/
2653structure EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5 where
2654  relativeData : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5
2655  relativeGeneratorOrthogonalOnTT : PeriodicRelativeTTGeneratorOrthogonalOnTT5
2656
2657/-- Relative-frame translated data plus the sharper generator-closure bridge.
2658This is the preferred mathematical target: prove closure once, then
2659orthogonality follows from the existing TT definition. -/
2660structure EncodedTTHessianLichnerowiczCoeffRelativeTranslatedClosureData5 where
2661  relativeData : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5
2662  relativeGeneratorClosure : PeriodicRelativeTTGeneratorClosure5
2663
2664/-- Generator closure supplies the orthogonality package required by the
2665conditional relative-frame TT-zero route. -/
2666def EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5.ofClosureData
2667    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedClosureData5) :
2668    EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5 where
2669  relativeData := D.relativeData
2670  relativeGeneratorOrthogonalOnTT :=
2671    PeriodicRelativeTTGeneratorOrthogonalOnTT5.ofClosure D.relativeGeneratorClosure
2672
2673/-- The shifted-generator closure theorem is now proved, so a relative-frame
2674translated certificate alone supplies the TT-zero package. -/
2675def EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5.ofRelativeTranslatedData
2676    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5) :
2677    EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5 where
2678  relativeData := D
2679  relativeGeneratorOrthogonalOnTT :=
2680    PeriodicRelativeTTGeneratorOrthogonalOnTT5.ofClosure
2681      periodicRelativeTTGeneratorClosure5_holds
2682
2683/-- Rowwise kernel data supplies the TT Hessian/Lichnerowicz operator-match
2684data. -/
2685def PeriodicTTHessianLichnerowiczMatchData5.ofKernelRowData
2686    (D : PeriodicTTHessianLichnerowiczKernelRowData5) :
2687    PeriodicTTHessianLichnerowiczMatchData5 where
2688  reggeHessianTT := periodicEdgeKernelOperator5 D.reggeHessianKernel
2689  latticeLichnerowiczTT := periodicEdgeKernelOperator5 D.latticeLichnerowiczKernel
2690  matches_on_tt := by
2691    intro ε hε
2692    exact periodicEdgeKernelOperator5_eq_of_row_eq
2693      D.reggeHessianKernel D.latticeLichnerowiczKernel ε
2694      (D.kernel_rows_match_on_tt ε hε)
2695
2696/-- Entrywise kernel data supplies rowwise kernel data. -/
2697def PeriodicTTHessianLichnerowiczKernelRowData5.ofEntryData
2698    (D : PeriodicTTHessianLichnerowiczKernelEntryData5) :
2699    PeriodicTTHessianLichnerowiczKernelRowData5 where
2700  reggeHessianKernel := D.reggeHessianKernel
2701  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2702  kernel_rows_match_on_tt := by
2703    intro ε _hε e
2704    have h :=
2705      periodicEdgeKernelOperator5_eq_of_kernel_eq
2706        D.reggeHessianKernel D.latticeLichnerowiczKernel
2707        D.kernel_entries_match ε
2708    exact congrFun h e
2709
2710/-- Residual-kernel vanishing on TT perturbations supplies rowwise kernel
2711matching on TT perturbations. -/
2712def PeriodicTTHessianLichnerowiczKernelRowData5.ofResidualTTZeroData
2713    (D : PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5) :
2714    PeriodicTTHessianLichnerowiczKernelRowData5 where
2715  reggeHessianKernel := D.reggeHessianKernel
2716  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2717  kernel_rows_match_on_tt := by
2718    intro ε hε e
2719    have hzero := congrFun (D.residual_zero_on_tt ε hε) e
2720    rw [periodicEdgeKernelOperator5_residual_eq_sub] at hzero
2721    exact sub_eq_zero.mp hzero
2722
2723/-- Residual-row generator-span data proves that the residual kernel annihilates
2724every TT perturbation. -/
2725def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofResidualRowSpanData
2726    (D : PeriodicTTHessianLichnerowiczResidualRowSpanData5) :
2727    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 where
2728  reggeHessianKernel := D.reggeHessianKernel
2729  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2730  residual_zero_on_tt := by
2731    intro ε hε
2732    funext e
2733    rcases D.residual_row_mem_generator_span e with ⟨coeff, hrow⟩
2734    rw [periodicEdgeKernelOperator5_eq_inner_row]
2735    rw [hrow]
2736    exact periodicLongitudinalTTSubspace5_inner_generatorMap_eq_zero ε hε coeff
2737
2738/-- Explicit residual-row coefficients supply residual-row span data. -/
2739def PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofRowCoeffData
2740    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffData5) :
2741    PeriodicTTHessianLichnerowiczResidualRowSpanData5 where
2742  reggeHessianKernel := D.reggeHessianKernel
2743  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2744  residual_row_mem_generator_span := by
2745    intro e
2746    exact ⟨D.residualRowCoeff e, D.residual_row_eq_generatorMap e⟩
2747
2748/-- Entrywise residual-row coefficients supply row-coefficient data. -/
2749def PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEntryData
2750    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5) :
2751    PeriodicTTHessianLichnerowiczResidualRowCoeffData5 where
2752  reggeHessianKernel := D.reggeHessianKernel
2753  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2754  residualRowCoeff := D.residualRowCoeff
2755  residual_row_eq_generatorMap := by
2756    intro e
2757    funext f
2758    exact D.residual_entry_eq_generatorMap e f
2759
2760/-- Raw scalar residual formulas supply entrywise residual-row coefficients. -/
2761def PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData
2762    (D : PeriodicTTHessianLichnerowiczResidualEntryFormulaData5) :
2763    PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5 where
2764  reggeHessianKernel := D.reggeHessianKernel
2765  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2766  residualRowCoeff := D.residualRowCoeff
2767  residual_entry_eq_generatorMap := by
2768    intro e f
2769    unfold periodicEdgeKernelResidual5
2770    exact D.residual_entry_formula e f
2771
2772/-- Encoded finite-index formulas supply the typed periodic raw scalar formula
2773data by transporting both kernels through `PeriodicTorus5.edgeEquiv`. -/
2774def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData
2775    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
2776    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 where
2777  reggeHessianKernel := encodedToPeriodicEdgeKernel5 D.reggeHessianKernel
2778  latticeLichnerowiczKernel := encodedToPeriodicEdgeKernel5 D.latticeLichnerowiczKernel
2779  residualRowCoeff := D.residualRowCoeff
2780  residual_entry_formula := by
2781    intro e f
2782    have h :=
2783      D.encoded_residual_entry_formula
2784        (PeriodicTorus5.edgeEquiv.symm e)
2785        (PeriodicTorus5.edgeEquiv.symm f)
2786    simpa [encodedToPeriodicEdgeKernel5] using h
2787
2788/-- Encoded residual-kernel certificates supply encoded raw scalar formula
2789data. -/
2790def EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofResidualKernelData
2791    (D : EncodedTTHessianLichnerowiczResidualKernelFormulaData5) :
2792    EncodedTTHessianLichnerowiczResidualEntryFormulaData5 where
2793  reggeHessianKernel := D.reggeHessianKernel
2794  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2795  residualRowCoeff := D.residualRowCoeff
2796  encoded_residual_entry_formula := by
2797    intro e f
2798    rw [← encodedEdgeKernelResidual5_apply D.reggeHessianKernel D.latticeLichnerowiczKernel e f]
2799    rw [← D.residualKernel_eq_sub e f]
2800    exact D.residualKernel_entry_formula e f
2801
2802/-- Displacement-row certificates supply encoded residual-kernel certificates by
2803using the edge displacement as the row coefficient index. -/
2804def EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofDispRowData
2805    (D : EncodedTTHessianLichnerowiczResidualDispRowFormulaData5) :
2806    EncodedTTHessianLichnerowiczResidualKernelFormulaData5 where
2807  reggeHessianKernel := D.reggeHessianKernel
2808  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2809  residualKernel := D.residualKernel
2810  residualRowCoeff := fun edge => D.residualDispCoeff edge.disp
2811  residualKernel_eq_sub := D.residualKernel_eq_sub
2812  residualKernel_entry_formula := by
2813    intro e f
2814    rw [D.residualKernel_row_translation e f]
2815    exact D.residual_origin_row_formula (PeriodicTorus5.edgeEquiv e).disp f
2816
2817/-- Seven-row origin-table certificates supply displacement-row certificates. -/
2818def EncodedTTHessianLichnerowiczResidualDispRowFormulaData5.ofOriginRowTableData
2819    (D : EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5) :
2820    EncodedTTHessianLichnerowiczResidualDispRowFormulaData5 where
2821  reggeHessianKernel := D.reggeHessianKernel
2822  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2823  residualKernel := D.residualKernel
2824  residualDispCoeff := D.residualDispCoeff
2825  residualKernel_eq_sub := D.residualKernel_eq_sub
2826  residualKernel_row_translation := by
2827    intro e f
2828    rw [D.residualKernel_row_translation e f]
2829    rw [D.residualOriginRow_eq_origin]
2830  residual_origin_row_formula := by
2831    intro disp f
2832    rw [← D.residualOriginRow_eq_origin disp f]
2833    exact D.residualOriginRow_entry_formula disp f
2834
2835/-- Typed-column origin-table certificates supply seven-row origin-table
2836certificates. -/
2837def EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData
2838    (D : EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5) :
2839    EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5 where
2840  reggeHessianKernel := D.reggeHessianKernel
2841  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2842  residualKernel := D.residualKernel
2843  residualOriginRow := fun rowDisp f =>
2844    D.residualOriginColumn
2845      rowDisp
2846      (PeriodicTorus5.edgeEquiv f).base
2847      (PeriodicTorus5.edgeEquiv f).disp
2848  residualDispCoeff := D.residualDispCoeff
2849  residualKernel_eq_sub := D.residualKernel_eq_sub
2850  residualOriginRow_eq_origin := by
2851    intro rowDisp f
2852    have hcol :
2853        ({ base := (PeriodicTorus5.edgeEquiv f).base,
2854            disp := (PeriodicTorus5.edgeEquiv f).disp } : PeriodicEdge5) =
2855          PeriodicTorus5.edgeEquiv f := by
2856      cases PeriodicTorus5.edgeEquiv f
2857      rfl
2858    have hidx :
2859        PeriodicTorus5.edgeEquiv.symm
2860          ({ base := (PeriodicTorus5.edgeEquiv f).base,
2861             disp := (PeriodicTorus5.edgeEquiv f).disp } : PeriodicEdge5) = f := by
2862      rw [hcol]
2863      simp
2864    rw [D.residualOriginColumn_eq_origin]
2865    rw [hidx]
2866  residualKernel_row_translation := D.residualKernel_row_translation
2867  residualOriginRow_entry_formula := by
2868    intro rowDisp f
2869    simpa using
2870      D.residualOriginColumn_entry_formula
2871        rowDisp
2872        (PeriodicTorus5.edgeEquiv f).base
2873        (PeriodicTorus5.edgeEquiv f).disp
2874
2875/-- Raw typed-column certificates supply typed-column origin-table certificates
2876by using `encodedEdgeKernelResidual5` as the residual matrix. -/
2877def EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData
2878    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
2879    EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5 where
2880  reggeHessianKernel := D.reggeHessianKernel
2881  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2882  residualKernel :=
2883    encodedEdgeKernelResidual5 D.reggeHessianKernel D.latticeLichnerowiczKernel
2884  residualOriginColumn := D.residualOriginColumn
2885  residualDispCoeff := D.residualDispCoeff
2886  residualKernel_eq_sub := by
2887    intro e f
2888    rfl
2889  residualOriginColumn_eq_origin := by
2890    intro rowDisp colBase colDisp
2891    rw [D.residualOriginColumn_eq_sub]
2892    rfl
2893  residualKernel_row_translation := D.encodedResidual_row_translation
2894  residualOriginColumn_entry_formula := D.residualOriginColumn_entry_formula
2895
2896/-- Coefficient-only origin-column formulas supply raw typed-column
2897certificates by reconstructing the origin residual table from the generator
2898map. -/
2899def EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5.ofCoeffOriginColumnData
2900    (D : EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5) :
2901    EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5 where
2902  reggeHessianKernel := D.reggeHessianKernel
2903  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2904  residualOriginColumn :=
2905    fun rowDisp colBase colDisp =>
2906      periodicTTNormalEquationGeneratorMap5
2907        (D.residualDispCoeff rowDisp)
2908        ({ base := colBase, disp := colDisp } : PeriodicEdge5)
2909  residualDispCoeff := D.residualDispCoeff
2910  residualOriginColumn_eq_sub := by
2911    intro rowDisp colBase colDisp
2912    exact (D.originColumn_entry_formula rowDisp colBase colDisp).symm
2913  encodedResidual_row_translation := by
2914    intro e f
2915    exact D.encodedResidual_entry_formula e f
2916  residualOriginColumn_entry_formula := by
2917    intro rowDisp colBase colDisp
2918    rfl
2919
2920/-- Translated coefficient-only formulas supply the previous coefficient-only
2921origin-column certificate by specializing the translated formula to the origin
2922edge. -/
2923def EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5.ofCoeffTranslatedData
2924    (D : EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5) :
2925    EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5 where
2926  reggeHessianKernel := D.reggeHessianKernel
2927  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2928  residualDispCoeff := D.residualDispCoeff
2929  originColumn_entry_formula := by
2930    intro rowDisp colBase colDisp
2931    have h :=
2932      D.encodedResidual_entry_formula
2933        (encodedOriginEdgeOfDisp5 rowDisp)
2934        (PeriodicTorus5.edgeEquiv.symm
2935          ({ base := colBase, disp := colDisp } : PeriodicEdge5))
2936    simpa [encodedEdgeKernelResidual5, encodedOriginEdgeOfDisp5_equiv] using h
2937  encodedResidual_entry_formula := D.encodedResidual_entry_formula
2938
2939/-- Relative translated coefficient-only formulas specialize to the same
2940origin-column formulas as the absolute translated surface.  This is only an
2941origin-row consequence: it does not assert the stronger absolute row formula. -/
2942def EncodedTTHessianLichnerowiczCoeffRelativeOriginColumnFormulaData5.ofCoeffRelativeTranslatedData
2943    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5) :
2944    EncodedTTHessianLichnerowiczCoeffRelativeOriginColumnFormulaData5 where
2945  reggeHessianKernel := D.reggeHessianKernel
2946  latticeLichnerowiczKernel := D.latticeLichnerowiczKernel
2947  residualDispCoeff := D.residualDispCoeff
2948  originColumn_entry_formula := by
2949    intro rowDisp colBase colDisp
2950    have h :=
2951      D.encodedResidual_relative_entry_formula
2952        (encodedOriginEdgeOfDisp5 rowDisp)
2953        (PeriodicTorus5.edgeEquiv.symm
2954          ({ base := colBase, disp := colDisp } : PeriodicEdge5))
2955    simpa [encodedEdgeKernelResidual5, encodedOriginEdgeOfDisp5_equiv,
2956      periodicRelativeColumnOfOriginDisp5] using h
2957
2958/-- Raw typed-column certificates supply seven-row origin-table certificates. -/
2959def EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofRawOriginColumnData
2960    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
2961    EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5 :=
2962  EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData
2963    (EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData D)
2964
2965/-- Seven-row origin-table certificates supply encoded residual-kernel
2966certificates. -/
2967def EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofOriginRowTableData
2968    (D : EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5) :
2969    EncodedTTHessianLichnerowiczResidualKernelFormulaData5 :=
2970  EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofDispRowData
2971    (EncodedTTHessianLichnerowiczResidualDispRowFormulaData5.ofOriginRowTableData D)
2972
2973/-- Typed-column origin-table certificates supply encoded residual-kernel
2974certificates. -/
2975def EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofOriginColumnTableData
2976    (D : EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5) :
2977    EncodedTTHessianLichnerowiczResidualKernelFormulaData5 :=
2978  EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofOriginRowTableData
2979    (EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData D)
2980
2981/-- Raw typed-column certificates supply encoded residual-kernel certificates. -/
2982def EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofRawOriginColumnData
2983    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
2984    EncodedTTHessianLichnerowiczResidualKernelFormulaData5 :=
2985  EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofOriginColumnTableData
2986    (EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData D)
2987
2988/-- Displacement-row certificates supply encoded raw scalar formula data. -/
2989def EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofDispRowData
2990    (D : EncodedTTHessianLichnerowiczResidualDispRowFormulaData5) :
2991    EncodedTTHessianLichnerowiczResidualEntryFormulaData5 :=
2992  EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofResidualKernelData
2993    (EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofDispRowData D)
2994
2995/-- Seven-row origin-table certificates supply encoded raw scalar formula data. -/
2996def EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginRowTableData
2997    (D : EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5) :
2998    EncodedTTHessianLichnerowiczResidualEntryFormulaData5 :=
2999  EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofDispRowData
3000    (EncodedTTHessianLichnerowiczResidualDispRowFormulaData5.ofOriginRowTableData D)
3001
3002/-- Typed-column origin-table certificates supply encoded raw scalar formula
3003data. -/
3004def EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginColumnTableData
3005    (D : EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5) :
3006    EncodedTTHessianLichnerowiczResidualEntryFormulaData5 :=
3007  EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginRowTableData
3008    (EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData D)
3009
3010/-- Raw typed-column certificates supply encoded raw scalar formula data. -/
3011def EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofRawOriginColumnData
3012    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
3013    EncodedTTHessianLichnerowiczResidualEntryFormulaData5 :=
3014  EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginColumnTableData
3015    (EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData D)
3016
3017
3018/-- Encoded residual-kernel certificates supply the typed periodic raw scalar
3019formula data. -/
3020def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedResidualKernelData
3021    (D : EncodedTTHessianLichnerowiczResidualKernelFormulaData5) :
3022    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 :=
3023  PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData
3024    (EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofResidualKernelData D)
3025
3026/-- Displacement-row certificates supply the typed periodic raw scalar formula
3027data. -/
3028def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofDispRowData
3029    (D : EncodedTTHessianLichnerowiczResidualDispRowFormulaData5) :
3030    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 :=
3031  PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedResidualKernelData
3032    (EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofDispRowData D)
3033
3034/-- Seven-row origin-table certificates supply the typed periodic raw scalar
3035formula data. -/
3036def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginRowTableData
3037    (D : EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5) :
3038    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 :=
3039  PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofDispRowData
3040    (EncodedTTHessianLichnerowiczResidualDispRowFormulaData5.ofOriginRowTableData D)
3041
3042/-- Typed-column origin-table certificates supply the typed periodic raw scalar
3043formula data. -/
3044def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginColumnTableData
3045    (D : EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5) :
3046    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 :=
3047  PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginRowTableData
3048    (EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData D)
3049
3050/-- Raw typed-column certificates supply the typed periodic raw scalar formula
3051data. -/
3052def PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofRawOriginColumnData
3053    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
3054    PeriodicTTHessianLichnerowiczResidualEntryFormulaData5 :=
3055  PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofOriginColumnTableData
3056    (EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData D)
3057
3058
3059
3060/-- Encoded finite-index formulas supply entrywise residual-row coefficients. -/
3061def PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofEncodedData
3062    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
3063    PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5 :=
3064  PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData
3065    (PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData D)
3066
3067/-- Encoded residual-kernel certificates supply entrywise residual-row
3068coefficients. -/
3069def PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofEncodedResidualKernelData
3070    (D : EncodedTTHessianLichnerowiczResidualKernelFormulaData5) :
3071    PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5 :=
3072  PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofEncodedData
3073    (EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofResidualKernelData D)
3074
3075/-- Raw scalar residual formulas supply row-coefficient data. -/
3076def PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofFormulaData
3077    (D : PeriodicTTHessianLichnerowiczResidualEntryFormulaData5) :
3078    PeriodicTTHessianLichnerowiczResidualRowCoeffData5 :=
3079  PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEntryData
3080    (PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData D)
3081
3082/-- Encoded finite-index formulas supply row-coefficient data. -/
3083def PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEncodedData
3084    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
3085    PeriodicTTHessianLichnerowiczResidualRowCoeffData5 :=
3086  PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofFormulaData
3087    (PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData D)
3088
3089/-- Entrywise residual-row coefficients supply residual-row span data. -/
3090def PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofEntryCoeffData
3091    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5) :
3092    PeriodicTTHessianLichnerowiczResidualRowSpanData5 :=
3093  PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofRowCoeffData
3094    (PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEntryData D)
3095
3096/-- Raw scalar residual formulas supply residual-row span data. -/
3097def PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofFormulaData
3098    (D : PeriodicTTHessianLichnerowiczResidualEntryFormulaData5) :
3099    PeriodicTTHessianLichnerowiczResidualRowSpanData5 :=
3100  PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofEntryCoeffData
3101    (PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData D)
3102
3103/-- Encoded finite-index formulas supply residual-row span data. -/
3104def PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofEncodedData
3105    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
3106    PeriodicTTHessianLichnerowiczResidualRowSpanData5 :=
3107  PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofFormulaData
3108    (PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData D)
3109
3110/-- Explicit residual-row coefficients supply residual-kernel zero-on-TT data. -/
3111def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofRowCoeffData
3112    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffData5) :
3113    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3114  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofResidualRowSpanData
3115    (PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofRowCoeffData D)
3116
3117/-- Entrywise residual-row coefficients supply residual-kernel zero-on-TT data. -/
3118def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofEntryCoeffData
3119    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5) :
3120    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3121  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofRowCoeffData
3122    (PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEntryData D)
3123
3124/-- Raw scalar residual formulas supply residual-kernel zero-on-TT data. -/
3125def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofFormulaData
3126    (D : PeriodicTTHessianLichnerowiczResidualEntryFormulaData5) :
3127    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3128  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofEntryCoeffData
3129    (PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData D)
3130
3131/-- Encoded finite-index formulas supply residual-kernel zero-on-TT data. -/
3132def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofEncodedData
3133    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
3134    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3135  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofFormulaData
3136    (PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData D)
3137
3138/-- Relative-frame translated certificates prove residual-kernel zero on TT once
3139the shifted-generator orthogonality lemma is supplied. -/
3140def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedTTZeroData
3141    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5) :
3142    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 where
3143  reggeHessianKernel := encodedToPeriodicEdgeKernel5 D.relativeData.reggeHessianKernel
3144  latticeLichnerowiczKernel := encodedToPeriodicEdgeKernel5 D.relativeData.latticeLichnerowiczKernel
3145  residual_zero_on_tt := by
3146    intro ε hε
3147    funext row
3148    rw [periodicEdgeKernelOperator5_eq_inner_row]
3149    have hrow :
3150        periodicEdgeKernelRowVector5
3151          (periodicEdgeKernelResidual5
3152            (encodedToPeriodicEdgeKernel5 D.relativeData.reggeHessianKernel)
3153            (encodedToPeriodicEdgeKernel5 D.relativeData.latticeLichnerowiczKernel))
3154          row =
3155        periodicRelativeTTNormalEquationGeneratorMap5 row
3156          (D.relativeData.residualDispCoeff row.disp) := by
3157      funext col
3158      unfold periodicEdgeKernelRowVector5 periodicEdgeKernelResidual5
3159        encodedToPeriodicEdgeKernel5 periodicRelativeTTNormalEquationGeneratorMap5
3160      simpa [encodedEdgeKernelResidual5] using
3161        D.relativeData.encodedResidual_relative_entry_formula
3162        (PeriodicTorus5.edgeEquiv.symm row)
3163        (PeriodicTorus5.edgeEquiv.symm col)
3164    rw [hrow]
3165    exact D.relativeGeneratorOrthogonalOnTT ε hε row
3166      (D.relativeData.residualDispCoeff row.disp)
3167
3168/-- Relative-frame translated closure data proves residual-kernel zero on TT. -/
3169def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedClosureData
3170    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedClosureData5) :
3171    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3172  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedTTZeroData
3173    (EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5.ofClosureData D)
3174
3175/-- Relative-frame translated certificates prove residual-kernel zero on TT
3176unconditionally, because the shifted-generator closure theorem is proved above. -/
3177def PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedData
3178    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5) :
3179    PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5 :=
3180  PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedTTZeroData
3181    (EncodedTTHessianLichnerowiczCoeffRelativeTranslatedTTZeroData5.ofRelativeTranslatedData D)
3182
3183/-- Entrywise kernel data supplies the TT Hessian/Lichnerowicz operator-match
3184data. -/
3185def PeriodicTTHessianLichnerowiczMatchData5.ofKernelEntryData
3186    (D : PeriodicTTHessianLichnerowiczKernelEntryData5) :
3187    PeriodicTTHessianLichnerowiczMatchData5 :=
3188  PeriodicTTHessianLichnerowiczMatchData5.ofKernelRowData
3189    (PeriodicTTHessianLichnerowiczKernelRowData5.ofEntryData D)
3190
3191/-- Residual-kernel vanishing on TT perturbations supplies the TT
3192Hessian/Lichnerowicz operator-match data. -/
3193def PeriodicTTHessianLichnerowiczMatchData5.ofResidualTTZeroData
3194    (D : PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5) :
3195    PeriodicTTHessianLichnerowiczMatchData5 :=
3196  PeriodicTTHessianLichnerowiczMatchData5.ofKernelRowData
3197    (PeriodicTTHessianLichnerowiczKernelRowData5.ofResidualTTZeroData D)
3198
3199/-- Relative-frame translated coefficient certificates supply TT
3200Hessian/Lichnerowicz operator-match data through the proved shifted-generator
3201closure theorem. -/
3202def PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData
3203    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5) :
3204    PeriodicTTHessianLichnerowiczMatchData5 :=
3205  PeriodicTTHessianLichnerowiczMatchData5.ofResidualTTZeroData
3206    (PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofCoeffRelativeTranslatedData D)
3207
3208/-- Residual-row generator-span data supplies the TT Hessian/Lichnerowicz
3209operator-match data. -/
3210def PeriodicTTHessianLichnerowiczMatchData5.ofResidualRowSpanData
3211    (D : PeriodicTTHessianLichnerowiczResidualRowSpanData5) :
3212    PeriodicTTHessianLichnerowiczMatchData5 :=
3213  PeriodicTTHessianLichnerowiczMatchData5.ofResidualTTZeroData
3214    (PeriodicTTHessianLichnerowiczKernelResidualTTZeroData5.ofResidualRowSpanData D)
3215
3216/-- Explicit residual-row coefficients supply TT Hessian/Lichnerowicz
3217operator-match data. -/
3218def PeriodicTTHessianLichnerowiczMatchData5.ofRowCoeffData
3219    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffData5) :
3220    PeriodicTTHessianLichnerowiczMatchData5 :=
3221  PeriodicTTHessianLichnerowiczMatchData5.ofResidualRowSpanData
3222    (PeriodicTTHessianLichnerowiczResidualRowSpanData5.ofRowCoeffData D)
3223
3224/-- Entrywise residual-row coefficients supply TT Hessian/Lichnerowicz
3225operator-match data. -/
3226def PeriodicTTHessianLichnerowiczMatchData5.ofEntryCoeffData
3227    (D : PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5) :
3228    PeriodicTTHessianLichnerowiczMatchData5 :=
3229  PeriodicTTHessianLichnerowiczMatchData5.ofRowCoeffData
3230    (PeriodicTTHessianLichnerowiczResidualRowCoeffData5.ofEntryData D)
3231
3232/-- Raw scalar residual formulas supply TT Hessian/Lichnerowicz operator-match
3233data. -/
3234def PeriodicTTHessianLichnerowiczMatchData5.ofFormulaData
3235    (D : PeriodicTTHessianLichnerowiczResidualEntryFormulaData5) :
3236    PeriodicTTHessianLichnerowiczMatchData5 :=
3237  PeriodicTTHessianLichnerowiczMatchData5.ofEntryCoeffData
3238    (PeriodicTTHessianLichnerowiczResidualRowCoeffEntryData5.ofFormulaData D)
3239
3240/-- Encoded finite-index formulas supply TT Hessian/Lichnerowicz operator-match
3241data. -/
3242def PeriodicTTHessianLichnerowiczMatchData5.ofEncodedData
3243    (D : EncodedTTHessianLichnerowiczResidualEntryFormulaData5) :
3244    PeriodicTTHessianLichnerowiczMatchData5 :=
3245  PeriodicTTHessianLichnerowiczMatchData5.ofFormulaData
3246    (PeriodicTTHessianLichnerowiczResidualEntryFormulaData5.ofEncodedData D)
3247
3248/-- Encoded residual-kernel certificates supply TT Hessian/Lichnerowicz
3249operator-match data. -/
3250def PeriodicTTHessianLichnerowiczMatchData5.ofEncodedResidualKernelData
3251    (D : EncodedTTHessianLichnerowiczResidualKernelFormulaData5) :
3252    PeriodicTTHessianLichnerowiczMatchData5 :=
3253  PeriodicTTHessianLichnerowiczMatchData5.ofEncodedData
3254    (EncodedTTHessianLichnerowiczResidualEntryFormulaData5.ofResidualKernelData D)
3255
3256/-- Displacement-row certificates supply TT Hessian/Lichnerowicz operator-match
3257data. -/
3258def PeriodicTTHessianLichnerowiczMatchData5.ofDispRowData
3259    (D : EncodedTTHessianLichnerowiczResidualDispRowFormulaData5) :
3260    PeriodicTTHessianLichnerowiczMatchData5 :=
3261  PeriodicTTHessianLichnerowiczMatchData5.ofEncodedResidualKernelData
3262    (EncodedTTHessianLichnerowiczResidualKernelFormulaData5.ofDispRowData D)
3263
3264/-- Seven-row origin-table certificates supply TT Hessian/Lichnerowicz
3265operator-match data. -/
3266def PeriodicTTHessianLichnerowiczMatchData5.ofOriginRowTableData
3267    (D : EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5) :
3268    PeriodicTTHessianLichnerowiczMatchData5 :=
3269  PeriodicTTHessianLichnerowiczMatchData5.ofDispRowData
3270    (EncodedTTHessianLichnerowiczResidualDispRowFormulaData5.ofOriginRowTableData D)
3271
3272/-- Typed-column origin-table certificates supply TT Hessian/Lichnerowicz
3273operator-match data. -/
3274def PeriodicTTHessianLichnerowiczMatchData5.ofOriginColumnTableData
3275    (D : EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5) :
3276    PeriodicTTHessianLichnerowiczMatchData5 :=
3277  PeriodicTTHessianLichnerowiczMatchData5.ofOriginRowTableData
3278    (EncodedTTHessianLichnerowiczResidualOriginRowTableFormulaData5.ofOriginColumnTableData D)
3279
3280/-- Raw typed-column certificates supply TT Hessian/Lichnerowicz operator-match
3281data. -/
3282def PeriodicTTHessianLichnerowiczMatchData5.ofRawOriginColumnData
3283    (D : EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5) :
3284    PeriodicTTHessianLichnerowiczMatchData5 :=
3285  PeriodicTTHessianLichnerowiczMatchData5.ofOriginColumnTableData
3286    (EncodedTTHessianLichnerowiczResidualOriginColumnTableFormulaData5.ofRawOriginColumnData D)
3287
3288/-- Coefficient-only origin-column certificates supply TT Hessian/Lichnerowicz
3289operator-match data by reconstructing the raw typed-column certificate. -/
3290def PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData
3291    (D : EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5) :
3292    PeriodicTTHessianLichnerowiczMatchData5 :=
3293  PeriodicTTHessianLichnerowiczMatchData5.ofRawOriginColumnData
3294    (EncodedTTHessianLichnerowiczRawOriginColumnFormulaData5.ofCoeffOriginColumnData D)
3295
3296/-- Translated coefficient-only certificates supply TT Hessian/Lichnerowicz
3297operator-match data through the derived coefficient origin-column certificate. -/
3298def PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData
3299    (D : EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5) :
3300    PeriodicTTHessianLichnerowiczMatchData5 :=
3301  PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData
3302    (EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5.ofCoeffTranslatedData D)
3303
3304/-- Operator equality on TT modes gives equality of the associated bilinear
3305forms whenever the right input is TT. -/
3306theorem periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5
3307    (D : PeriodicTTHessianLichnerowiczMatchData5)
3308    (ε η : PeriodicEdgePerturbation5)
3309    (hη : PeriodicLongitudinalTTSubspace5 η) :
3310    periodicTTOperatorBilinear5 D.reggeHessianTT ε η =
3311      periodicTTOperatorBilinear5 D.latticeLichnerowiczTT ε η := by
3312  unfold periodicTTOperatorBilinear5
3313  rw [D.matches_on_tt η hη]
3314
3315/-- Operator equality on TT modes gives equality of the quadratic TT energy. -/
3316theorem periodicTTHessianLichnerowicz_quadratic_eq_of_matchData5
3317    (D : PeriodicTTHessianLichnerowiczMatchData5)
3318    (ε : PeriodicEdgePerturbation5)
3319    (hε : PeriodicLongitudinalTTSubspace5 ε) :
3320    periodicTTOperatorBilinear5 D.reggeHessianTT ε ε =
3321      periodicTTOperatorBilinear5 D.latticeLichnerowiczTT ε ε :=
3322  periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5 D ε ε hε
3323
3324/-- Coefficient-only origin-column certificates give equality of the associated
3325bilinear forms whenever the right input is TT. -/
3326theorem periodicTTHessianLichnerowicz_bilinear_eq_of_coeffOriginColumnData5
3327    (D : EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5)
3328    (ε η : PeriodicEdgePerturbation5)
3329    (hη : PeriodicLongitudinalTTSubspace5 η) :
3330    periodicTTOperatorBilinear5
3331        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D).reggeHessianTT ε η =
3332      periodicTTOperatorBilinear5
3333        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D).latticeLichnerowiczTT ε η :=
3334  periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5
3335    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D) ε η hη
3336
3337/-- Coefficient-only origin-column certificates give equality of the quadratic
3338TT energy. -/
3339theorem periodicTTHessianLichnerowicz_quadratic_eq_of_coeffOriginColumnData5
3340    (D : EncodedTTHessianLichnerowiczCoeffOriginColumnFormulaData5)
3341    (ε : PeriodicEdgePerturbation5)
3342    (hε : PeriodicLongitudinalTTSubspace5 ε) :
3343    periodicTTOperatorBilinear5
3344        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D).reggeHessianTT ε ε =
3345      periodicTTOperatorBilinear5
3346        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D).latticeLichnerowiczTT ε ε :=
3347  periodicTTHessianLichnerowicz_quadratic_eq_of_matchData5
3348    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffOriginColumnData D) ε hε
3349
3350/-- Translated coefficient-only certificates give equality of the associated
3351bilinear forms whenever the right input is TT. -/
3352theorem periodicTTHessianLichnerowicz_bilinear_eq_of_coeffTranslatedData5
3353    (D : EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5)
3354    (ε η : PeriodicEdgePerturbation5)
3355    (hη : PeriodicLongitudinalTTSubspace5 η) :
3356    periodicTTOperatorBilinear5
3357        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D).reggeHessianTT ε η =
3358      periodicTTOperatorBilinear5
3359        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D).latticeLichnerowiczTT ε η :=
3360  periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5
3361    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D) ε η hη
3362
3363/-- Translated coefficient-only certificates give equality of the quadratic TT
3364energy. -/
3365theorem periodicTTHessianLichnerowicz_quadratic_eq_of_coeffTranslatedData5
3366    (D : EncodedTTHessianLichnerowiczCoeffTranslatedFormulaData5)
3367    (ε : PeriodicEdgePerturbation5)
3368    (hε : PeriodicLongitudinalTTSubspace5 ε) :
3369    periodicTTOperatorBilinear5
3370        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D).reggeHessianTT ε ε =
3371      periodicTTOperatorBilinear5
3372        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D).latticeLichnerowiczTT ε ε :=
3373  periodicTTHessianLichnerowicz_quadratic_eq_of_matchData5
3374    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffTranslatedData D) ε hε
3375
3376/-- Relative-frame translated coefficient-only certificates give equality of the
3377associated bilinear forms whenever the right input is TT. -/
3378theorem periodicTTHessianLichnerowicz_bilinear_eq_of_coeffRelativeTranslatedData5
3379    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5)
3380    (ε η : PeriodicEdgePerturbation5)
3381    (hη : PeriodicLongitudinalTTSubspace5 η) :
3382    periodicTTOperatorBilinear5
3383        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D).reggeHessianTT ε η =
3384      periodicTTOperatorBilinear5
3385        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D).latticeLichnerowiczTT ε η :=
3386  periodicTTHessianLichnerowicz_bilinear_eq_of_matchData5
3387    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D) ε η hη
3388
3389/-- Relative-frame translated coefficient-only certificates give equality of the
3390quadratic TT energy. -/
3391theorem periodicTTHessianLichnerowicz_quadratic_eq_of_coeffRelativeTranslatedData5
3392    (D : EncodedTTHessianLichnerowiczCoeffRelativeTranslatedFormulaData5)
3393    (ε : PeriodicEdgePerturbation5)
3394    (hε : PeriodicLongitudinalTTSubspace5 ε) :
3395    periodicTTOperatorBilinear5
3396        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D).reggeHessianTT ε ε =
3397      periodicTTOperatorBilinear5
3398        (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D).latticeLichnerowiczTT ε ε :=
3399  periodicTTHessianLichnerowicz_quadratic_eq_of_matchData5
3400    (PeriodicTTHessianLichnerowiczMatchData5.ofCoeffRelativeTranslatedData D) ε hε
3401
3402theorem periodicFreudenthalTTOrthogonalDecompositionTargetAtN5_to_target
3403    (GaugePotential : Type) (gaugeMap : GaugePotential → PeriodicEdgePerturbation5) :
3404    PeriodicFreudenthalTTOrthogonalDecompositionTargetAtN5 GaugePotential gaugeMap →
3405      PeriodicFreudenthalTTDecompositionTargetAtN5
3406        PeriodicConformalLogSubspace5
3407        (PeriodicGaugeSubspace5 GaugePotential gaugeMap)
3408        (PeriodicTTOrthogonal5 GaugePotential gaugeMap) := by
3409  intro h
3410  exact h
3411
3412/-- Session 215 scaffold endpoint for Track 1.D. -/
3413def Track1DTensorShearScaffoldEndpoint : Prop :=
3414  Nonempty (∀ K : Triangulation3D, VertexPotential K → EdgePerturbation K) ∧
3415    Nonempty (EncodedEdgePerturbation5 ≃ PeriodicEdgePerturbation5) ∧
3416    (∀ h v : ℝ, h ≠ v →
3417      ¬ ∃ ξa ξb ξc ξd : ℝ,
3418        (ξa + ξb) / 2 = h ∧
3419        (ξc + ξd) / 2 = h ∧
3420        (ξb + ξc) / 2 = v ∧
3421        (ξd + ξa) / 2 = v)
3422
3423theorem track1D_tensorShearScaffoldEndpoint_holds :
3424    Track1DTensorShearScaffoldEndpoint := by
3425  constructor
3426  · exact ⟨fun K => conformalEdgeLogStrain K⟩
3427  · constructor
3428    · exact ⟨periodicEdgePerturbationEquiv5⟩
3429    · intro h v hne
3430      exact nontrivial_rectangle_shear_not_vertexConformal h v hne
3431
3432end
3433
3434end TensorShearSector
3435end Gravity
3436end IndisputableMonolith
3437