IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation

   1import Mathlib
   2import IndisputableMonolith.Geometry.SchlaefliN
   3import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   4import IndisputableMonolith.Gravity.Analysis.ReggeEdgeStencil4D
   5import IndisputableMonolith.Gravity.Analysis.EdgeTTDecomposition4D
   6import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
   7import IndisputableMonolith.Gravity.Analysis.ReggeBlochM2Symbol4D
   8import IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight
   9import IndisputableMonolith.Gravity.Analysis.Regge4DTorusContinuumLimit
  10import IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser
  11import IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser
  12import IndisputableMonolith.Gravity.Analysis.Regge4DSchlaefliPathwise
  13
  14/-!
  15# 4D Regge flat second variation (Schläfli elevation status)
  16
  17Mirrors the 3D `ReggeTTFlatSecondVariation` contract: Gate A2 elevates the
  18true nonlinear Regge action to a Schläfli-reduced edge Hessian.  In 3D that
  19elevation is THEOREM (`tetraSchlaefliSixEdgeClosedForm` →
  20`trueReggeAction_secondVariation_flat_schlaefli`).  In 4D the flat-seed
  21Freudenthal flat closed form and flat directional Schläfli kill are
  22THEOREM in `Regge4DSchlaefliPathwise`
  23(`freudenthal4SimplexFlatSchlaefli`,
  24`freudenthal4SimplexFlatDirectionalSchlaefli`, seed-angle `HasDerivAt`);
  25the full off-flat pathwise closed form remains absent, so elevation of
  26the nonlinear action stays OPEN.
  27
  28## Tier tags (binding)
  29
  30* THEOREM: candidate reduced Hessian identified with the assembled /
  31  distinct-hinge geometry object; Bloch continuum face of that candidate
  32  on Frobenius-normalized axis TT at `symbolDir` equals `-1/16`; that
  33  face differs from frozen EH `-1/4`; density dictionary survivor is `1`.
  34* THEOREM: flat Freudenthal 4-simplex Schläfli summand table with
  35  vanishing column sums, seed-hinge geometric match, seed-angle
  36  `HasDerivAt`, and flat directional kill along every affine velocity
  37  (`Regge4DSchlaefliPathwise`).
  38* OPEN: full off-flat `Freudenthal4SimplexPathwiseSchlaefli` and therefore
  39  `Regge4DSchlafliElevationToCandidate` (nonlinear `S''(0)` equals the
  40  candidate).
  41* Does **not** flip `gap_action_recovery`.
  42* Does **not** inhabit `S_RS_converges_EH_4d`.
  43
  44## Why prior paths do not close this gap
  45
  46* Distinct-hinge fold: symbolDir isotropic at face `-1/16`; e0 plus `= 0`.
  47* Full two-jet: equals `A0·K2` (`K0 = 0`); no repair.
  48* Path B mean-local: equals distinct-hinge (vacuous); position-resolved
  49  breaks symbolDir isotropy.
  50* Density dictionary survivor already `1`.
  51
  52Residual is therefore Schläfli elevation of the nonlinear action, not
  53another incidence rescale or fitted factor.
  54-/
  55
  56namespace IndisputableMonolith
  57namespace Gravity
  58namespace Analysis
  59namespace Regge4DFlatSecondVariation
  60
  61open ReggeFlat4DHessianAssembly
  62open ReggeEdgeStencil4D
  63open EdgeTTDecomposition4D (axisTTPlus axisTTCross)
  64open ReggeBlochTransportedAllOrbit4D
  65open ReggeBlochM2Symbol4D (symbolDir)
  66open Regge4DContinuumPreflight
  67open Regge4DTorusContinuumLimit
  68open Regge4DTensorAlgebraicCloser
  69open Regge4DTransportedAlgebraicCloser (symbolDir_normSq)
  70open Geometry.SchlaefliN
  71open ReggeHinge4DDihedralKernel
  72open Regge4DSchlaefliPathwise
  73
  74noncomputable section
  75
  76/-- Local alias: preflight `Mat4`. -/
  77abbrev Mat4 := Regge4DContinuumPreflight.Mat4
  78
  79/-! ## §0. Flat-seed Schläfli progress (from Regge4DSchlaefliPathwise) -/
  80
  81theorem flat_freudenthal_schlaefli_present :
  82    freudenthal4SimplexFlatSchlaefliPresent = true :=
  83  freudenthal4SimplexFlatSchlaefliPresent_true
  84
  85theorem flat_freudenthal_schlaefli_identity (e : Fin 10) :
  86    (∑ h : Fin 10, flatSchlaefliSummand h e) = 0 :=
  87  freudenthal4SimplexFlatSchlaefli e
  88
  89theorem flat_freudenthal_directional_schlaefli_present :
  90    freudenthal4SimplexFlatDirectionalSchlaefliPresent = true :=
  91  freudenthal4SimplexFlatDirectionalSchlaefliPresent_true
  92
  93/-- Gate A2-style flat directional kill, re-exported for elevation wiring. -/
  94theorem flat_freudenthal_directional_schlaefli (v : Fin 10 → ℝ) :
  95    (∑ h : Fin 10, hingeAreaFlat h * flatDirectionalAngleDeriv v h) = 0 :=
  96  freudenthal4SimplexFlatDirectionalSchlaefli v
  97
  98theorem flat_freudenthal_seed_angle_hasDerivAt (k : Fin 10) :
  99    HasDerivAt (fun t : ℝ => seedDihedralAngle (coordPath k t))
 100      (angleKernel k) (seedFlatSqEdges k) :=
 101  hasDerivAt_seedDihedralAngle_coord k
 102
 103/-! ## §1. Candidate Schläfli-reduced Hessian (geometry-derived) -/
 104
 105/-- Zero-momentum candidate: orbit-count × Heron × star-deficit class
 106quadratic already assembled from committed geometry kernels. -/
 107def schlaefliCandidateZeroMom (H : Mat4) : ℝ :=
 108  trueWeightZeroMomQuadratic H
 109
 110/-- Finite-momentum candidate: distinct-hinge (`1/r_τ`) transported Bloch
 111fold of the same true-weight kernels.  This is the object that would equal
 112`(2/N⁴)·S''_nonlinear` under a 3D-style Schläfli elevation + cell-sum
 113dictionary (cf. `SchlafliElevationToDistinctHingeOpen`). -/
 114def schlaefliCandidateFold (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
 115  blochFoldAllDistinctHinge H m
 116
 117theorem schlaefliCandidateZeroMom_eq (H : Mat4) :
 118    schlaefliCandidateZeroMom H = trueWeightZeroMomQuadratic H :=
 119  rfl
 120
 121theorem schlaefliCandidateFold_eq (H : Mat4) (m : Fin 4 → ℝ) :
 122    schlaefliCandidateFold H m = blochFoldAllDistinctHinge H m :=
 123  rfl
 124
 125theorem schlaefliCandidate_vanishes_on_axisTTPlus :
 126    schlaefliCandidateZeroMom axisTTPlus = 0 :=
 127  trueWeightZeroMomQuadratic_axisTTPlus
 128
 129theorem schlaefliCandidate_vanishes_on_decoyGauge :
 130    schlaefliCandidateZeroMom decoyGauge = 0 :=
 131  trueWeightZeroMomQuadratic_decoyGauge
 132
 133/-! ## §2. Missing 4D Schläfli identity (typed OPEN) -/
 134
 135/-- **Named missing identity** (not a Lean theorem in this library).
 136
 137Pathwise Schläfli on every Freudenthal / Kuhn 4-simplex, squared-edge
 138coordinates:
 139
 140```
 141  ∀ σ 4-simplex, ∀ e ∈ edges(σ), at every nondegenerate path point,
 142    Σ_{h ⊂ σ} A_h(σ) · (∂θ_{σ,h} / ∂ℓ²_e) = 0
 143```
 144
 145(`nH = nE = 10` instance of `SchlaefliN.SchlaefliIdentityN` with
 146measures = hinge areas and `dTheta_dL` = squared-edge partials of the
 1474-simplex dihedrals).
 148
 1493D analog (THEOREM):
 150`Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm`.
 151
 152Flat-seed algebraic closed form and flat directional kill are THEOREM in
 153`Regge4DSchlaefliPathwise` (non-vacuous positive-area witness; seed-angle
 154`HasDerivAt`).  Full off-flat pathwise closed form along a general
 155nondegenerate path remains absent
 156(`freudenthal4SimplexPathwiseSchlaefliPresent` stays `false`).  Do not
 157inhabit a vacuous `Prop` shell. -/
 158theorem Freudenthal4SimplexPathwiseSchlaefli_absent :
 159    freudenthal4SimplexPathwiseSchlaefliPresent = false :=
 160  freudenthal4SimplexPathwiseSchlaefliPresent_false
 161
 162/-- Interface readiness only: once a concrete `SchlaefliDataN 10 10`
 163witness with `SchlaefliIdentityN` is supplied, the angle term dies.
 164This does **not** construct such a witness for Freudenthal 4-simplices. -/
 165theorem schlaefliN_interface_ready (D : SchlaefliDataN 10 10)
 166    (hS : SchlaefliIdentityN D) (e : Fin 10) :
 167    ∑ h : Fin 10, (D.hinge h).measure * D.dTheta_dL h e = 0 :=
 168  schlaefliN_kills_angle_term D hS e
 169
 170/-! ## §3. Elevation obligation (OPEN; not a tautology) -/
 171
 172/-- Independent nonlinear flat second variation type. -/
 173abbrev NonlinearFlatSecondVariation4D :=
 174  Regge4DTorusContinuumLimit.NonlinearSecondVariation4D
 175
 176/-- **OPEN.** Schläfli elevation: there exists an independent nonlinear
 177`S''` derived from the edge-length Regge action by the 4D pathwise
 178Schläfli kill (mirroring
 179`trueReggeAction_secondVariation_flat_schlaefli`) such that for every
 180non-aliased mode,
 181`(2/N⁴) · S''(N,m,E) = schlaefliCandidateFold E (realMode N m)`.
 182
 183Falsifier for a fake inhabit: setting
 184`S'' := (N⁴/2) · schlaefliCandidateFold` without a derivation from
 185`Freudenthal4SimplexPathwiseSchlaefli` and the nonlinear action. -/
 186def Regge4DSchlafliElevationToCandidate : Prop :=
 187  ∃ S'' : NonlinearFlatSecondVariation4D,
 188    ∀ (N : ℕ) [NeZero N] (m : IntMode4) (E : Mat4),
 189      (∃ i : Fin 4, ¬ (N : ℤ) ∣ 2 * m i) →
 190        ttSecondDifferenceDensityWeight N * S'' N m E =
 191          schlaefliCandidateFold E (realMode N m)
 192
 193/-- Alias retained for downstream imports. -/
 194def Regge4DSchlafliFiniteMomentumOpen : Prop :=
 195  Regge4DSchlafliElevationToCandidate
 196
 197def Regge4DSchlafliBridgeOpen : Prop :=
 198  Regge4DSchlafliElevationToCandidate
 199
 200/-- Compatibility with the torus-limit elevation Prop. -/
 201theorem elevation_iff_torus_open :
 202    Regge4DSchlafliElevationToCandidate ↔
 203      SchlafliElevationToDistinctHingeOpen := by
 204  constructor
 205  · intro ⟨S'', hS⟩
 206    refine ⟨S'', ?_⟩
 207    intro N _ m E hna
 208    have h := hS N m E hna
 209    simpa [schlaefliCandidateFold, canonicalFiniteH4D] using h
 210  · intro ⟨S'', hS⟩
 211    refine ⟨S'', ?_⟩
 212    intro N _ m E hna
 213    have h := hS N m E hna
 214    simpa [schlaefliCandidateFold, canonicalFiniteH4D] using h
 215
 216/-! ## §4. Bloch evaluation of the candidate (THEOREM) -/
 217
 218/-- Raw distinct-hinge m² on axis TT plus / `symbolDir` is `-1/4`. -/
 219theorem candidate_m2_axisTTPlus_symbolDir :
 220    distinctHingeMomentForm axisTTPlus symbolDir = (-1 / 4 : ℝ) :=
 221  distinctHingeMomentForm_axisTTPlus_symbolDir
 222
 223/-- Continuum-facing coefficient after Frobenius pin and `/|symbolDir|²`:
 224`-1/16`. -/
 225theorem candidate_continuumFace_normalizedTT_symbolDir :
 226    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
 227        (∑ i : Fin 4, symbolDir i * symbolDir i) =
 228      (-1 / 16 : ℝ) :=
 229  continuumFace_normalizedPlus_symbolDir
 230
 231/-- Frozen EH target. -/
 232theorem eh_target_neg_quarter :
 233    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) :=
 234  einsteinHilbertTTCoefficient4D_eq
 235
 236/-- **THEOREM (falsifier arithmetic).** The candidate's continuum face on
 237normalized TT at `symbolDir` is `-1/16`, which is not the frozen EH
 238coefficient `-1/4`.  Density dictionary survivor is already `1`. -/
 239theorem candidate_face_ne_eh :
 240    (-1 / 16 : ℝ) ≠ einsteinHilbertTTCoefficient4D ∧
 241      survivingDictionaryFactor4D = 1 :=
 242  ⟨by rw [einsteinHilbertTTCoefficient4D_eq]; norm_num, rfl⟩
 243
 244/-- Packaged claim
 245“Schläfli elevation to the distinct-hinge candidate restores EH `-1/4`”.
 246
 247Falsifier: if elevation held, the continuum symbol would be the candidate
 248face `-1/16` (dictionary survivor `1`), contradicting
 249`einsteinHilbertTTCoefficient4D = -1/4` on the axis TT / `symbolDir`
 250witness. -/
 251def SchlaefliElevationToCandidateClosesEH : Prop :=
 252  Regge4DSchlafliElevationToCandidate ∧
 253    Regge4DContinuumEHTarget
 254
 255theorem schlaefli_elevation_to_candidate_misses_eh_face :
 256    (-1 / 16 : ℝ) ≠ einsteinHilbertTTCoefficient4D :=
 257  candidate_face_ne_eh.1
 258
 259/-- Retained name: former tautology `assembled = assembled` is retired.
 260The live elevation obligation is `Regge4DSchlafliElevationToCandidate`. -/
 261def Regge4DSchlafliSecondVariation : Prop :=
 262  Regge4DSchlafliElevationToCandidate
 263
 264/-! ## §5. Status (honesty flags) -/
 265
 266structure Regge4DFlatSecondVariationStatus where
 267  candidateIdentified : Bool
 268  candidateBlochFaceEvaluated : Bool
 269  freudenthal4FlatSchlaefliPresent : Bool
 270  freudenthal4FlatDirectionalPresent : Bool
 271  freudenthal4PathwiseSchlaefliPresent : Bool
 272  schlafliElevationOpen : Bool
 273  gapActionRecovery : Bool
 274
 275def regge4DFlatSecondVariationStatus : Regge4DFlatSecondVariationStatus where
 276  candidateIdentified := true
 277  candidateBlochFaceEvaluated := true
 278  freudenthal4FlatSchlaefliPresent := true
 279  freudenthal4FlatDirectionalPresent := true
 280  freudenthal4PathwiseSchlaefliPresent := false
 281  schlafliElevationOpen := true
 282  gapActionRecovery := false
 283
 284theorem regge4DFlatSecondVariationStatus_flags :
 285    regge4DFlatSecondVariationStatus.candidateIdentified = true ∧
 286      regge4DFlatSecondVariationStatus.candidateBlochFaceEvaluated = true ∧
 287        regge4DFlatSecondVariationStatus.freudenthal4FlatSchlaefliPresent =
 288          true ∧
 289          regge4DFlatSecondVariationStatus.freudenthal4FlatDirectionalPresent =
 290            true ∧
 291            regge4DFlatSecondVariationStatus.freudenthal4PathwiseSchlaefliPresent =
 292              false ∧
 293              regge4DFlatSecondVariationStatus.schlafliElevationOpen = true ∧
 294                regge4DFlatSecondVariationStatus.gapActionRecovery = false := by
 295  decide
 296
 297/-- Honesty: full pathwise absent; elevation OPEN; gap stays false. -/
 298theorem schlafli_does_not_flip_gap :
 299    regge4DFlatSecondVariationStatus.freudenthal4PathwiseSchlaefliPresent =
 300        false ∧
 301      regge4DFlatSecondVariationStatus.schlafliElevationOpen = true ∧
 302        regge4DFlatSecondVariationStatus.gapActionRecovery = false :=
 303  ⟨rfl, rfl, rfl⟩
 304
 305end
 306
 307end Regge4DFlatSecondVariation
 308end Analysis
 309end Gravity
 310end IndisputableMonolith
 311