IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D

   1import Mathlib
   2import IndisputableMonolith.Geometry.FourTetSignedDeficit
   3import IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   5
   6/-!
   7# Wave B residual R1: mesh geometricDeficit identified (no xRatio)
   8
   9QG full-completion session, Wave B attack on
  10`TypedResidual_mesh_geometricDeficit_identified` from
  11`plans/QG_WaveB_Gap1_Residual_DAG_Draft_20260721.txt`.
  12
  13## DAG Prop vs Lean shape (recorded divergence)
  14
  15The DAG draft asked for `∃ δ : HingeCarrier → ℝ` that is the signed
  16Regge-convention hinge deficit of the recognition Freudenthal mesh
  17carrier, free of `xRatio` / `log xRatio`. Lean has no declaration
  18`HingeCarrier`, and `RecognitionFreudenthalMesh4D` does not yet expose a
  19per-hinge `deficitAngle` deformation family.
  20
  21Honest binding used here:
  22* deformation carrier `ℝ` with `FourTetSignedDeficit.starDeficit`
  23  (signed Regge-convention deficit from squared-edge geometry;
  24  odd, flat-vanishing, sign-certified);
  25* mesh context via `ExactJEqualsTrueReggeHessian` on
  26  `canonicalRecognitionMesh` (`exactJActionOnMesh` /
  27  `meshTrueReggeQuadraticHessian`);
  28* Freudenthal seed flatness `star_flat_angle_sum_two_pi` (banked
  29  `C-p1-regge-star-kernel-seed`).
  30
  31OPEN remainder after R1 (not a Prop shell): lift `starDeficit` onto
  32`ReggeActionConcrete.deficitAngle` on an encoded triangulation of the
  33recognition Freudenthal mesh. That join is not yet expressible
  34(`RecognitionFreudenthalMesh4D` has no triangulation field;
  35`FourTetSignedDeficit` stops at the abstract-star convention note).
  36Recorded only by `encodedFreudenthalLiftOpen := true` below.
  37
  38Does **not** flip `gap1_bridge_derived`. Does **not** inhabit
  39`DeficitSourceConstitutiveCoupling`. Does **not** claim
  40`recognition_ratio_derived`.
  41-/
  42
  43namespace IndisputableMonolith
  44namespace Gravity
  45namespace Analysis
  46namespace RecognitionMeshGeometricDeficit4D
  47
  48open Geometry.FourTetSignedDeficit
  49open Geometry.DihedralDerivatives
  50open RecognitionMeshExactJBridge4D
  51open ReggeHinge4DStarKernel
  52
  53noncomputable section
  54
  55/-! ## §1. Geometry-first deficit on the star deformation carrier -/
  56
  57/-- Mesh geometric deficit: the banked signed Regge-convention star
  58deficit as a function of the deformation parameter. Constructed from
  59squared-edge / dihedral geometry (`starSq`, `dihedralAngle3Sq`); no
  60`xRatio` or `Real.log` appears in the definition. -/
  61def meshGeometricDeficit : ℝ → ℝ :=
  62  starDeficit
  63
  64theorem meshGeometricDeficit_eq_starDeficit (h : ℝ) :
  65    meshGeometricDeficit h = starDeficit h := rfl
  66
  67/-- Geometry-first closed form (arcsin), free of ratio fields. -/
  68theorem meshGeometricDeficit_eq_arcsin (h : ℝ) :
  69    meshGeometricDeficit h = 4 * Real.arcsin h :=
  70  starDeficit_eq_arcsin h
  71
  72/-- Regge convention: `2π - 4 * dihedralAngle3Sq` on the star data. -/
  73theorem meshGeometricDeficit_regge_convention (h : ℝ) :
  74    meshGeometricDeficit h =
  75      2 * Real.pi - 4 * dihedralAngle3Sq (starSq (starP h)) 0 :=
  76  rfl
  77
  78theorem meshGeometricDeficit_odd (h : ℝ) :
  79    meshGeometricDeficit (-h) = -meshGeometricDeficit h :=
  80  starDeficit_odd h
  81
  82theorem meshGeometricDeficit_flat : meshGeometricDeficit 0 = 0 :=
  83  starDeficit_flat
  84
  85theorem meshGeometricDeficit_sign (h : ℝ) :
  86    (0 < h → 0 < meshGeometricDeficit h) ∧
  87      (h < 0 → meshGeometricDeficit h < 0) :=
  88  fourTet_deficit_sign h
  89
  90/-! ## §2. Typed residual R1 -/
  91
  92/-- **R1.** Mesh geometric deficit identified from exact-J / Regge star
  93geometry (no xRatio).
  94
  95Inhabits the DAG residual under the recorded carrier reshape: `δ` is
  96`starDeficit` on the deformation parameter, the recognition mesh supplies
  97the exact-J = true-Regge Hessian identity, and the Freudenthal seed star
  98is flat (`2π`). -/
  99def TypedResidual_mesh_geometricDeficit_identified : Prop :=
 100  ∃ δ : ℝ → ℝ,
 101    δ = starDeficit ∧
 102      (∀ h : ℝ, δ (-h) = -δ h) ∧
 103        δ 0 = 0 ∧
 104          (∀ h : ℝ, (0 < h → 0 < δ h) ∧ (h < 0 → δ h < 0)) ∧
 105            ExactJEqualsTrueReggeHessian ∧
 106              starFlatAngleSum = 2 * Real.pi
 107
 108/-- **THEOREM:** R1 closed. -/
 109theorem typedResidual_mesh_geometricDeficit_identified_closed :
 110    TypedResidual_mesh_geometricDeficit_identified := by
 111  refine ⟨starDeficit, rfl, starDeficit_odd, starDeficit_flat, ?_,
 112    exactJEqualsTrueReggeHessian_holds, star_flat_angle_sum_two_pi⟩
 113  intro h
 114  exact fourTet_deficit_sign h
 115
 116/-- Named alias matching the DAG residual title. -/
 117theorem TypedResidual_mesh_geometricDeficit_identified_closed :
 118    TypedResidual_mesh_geometricDeficit_identified :=
 119  typedResidual_mesh_geometricDeficit_identified_closed
 120
 121/-! ## §3. Decoys / falsifiers (DAG) -/
 122
 123/-- **Decoy:** any even-in-`h` candidate (ledger-style deficit families)
 124cannot equal the signed mesh geometric deficit on a punctured interval.
 125Banked as `even_cannot_match_starDeficit`. -/
 126theorem decoy_even_function_ne_mesh_geometricDeficit
 127    (g : ℝ → ℝ) (heven : ∀ h : ℝ, g (-h) = g h) :
 128    ¬ (∀ h : ℝ, 0 < |h| → |h| < 1 → g h = meshGeometricDeficit h) :=
 129  even_cannot_match_starDeficit g heven
 130
 131/-- **Decoy:** `δ := log(positedRatio) / κ` with an even posited ratio
 132(the wrong shortcut that smuggles a ratio field into the deficit) cannot
 133match `starDeficit` / `meshGeometricDeficit` on a punctured interval. -/
 134theorem decoy_log_even_ratio_over_kappa_ne_starDeficit
 135    (r : ℝ → ℝ) (κ : ℝ) (_hκ : κ ≠ 0)
 136    (_hr_pos : ∀ h : ℝ, 0 < r h)
 137    (hr_even : ∀ h : ℝ, r (-h) = r h) :
 138    ¬ (∀ h : ℝ, 0 < |h| → |h| < 1 →
 139        Real.log (r h) / κ = meshGeometricDeficit h) := by
 140  let g : ℝ → ℝ := fun h => Real.log (r h) / κ
 141  have heven : ∀ h : ℝ, g (-h) = g h := by
 142    intro h
 143    dsimp [g]
 144    rw [hr_even h]
 145  exact decoy_even_function_ne_mesh_geometricDeficit g heven
 146
 147/-- Package: both DAG decoys. -/
 148theorem adversarial_decoys_mesh_geometricDeficit :
 149    (∀ (g : ℝ → ℝ), (∀ h, g (-h) = g h) →
 150      ¬ (∀ h, 0 < |h| → |h| < 1 → g h = meshGeometricDeficit h)) ∧
 151      (∀ (r : ℝ → ℝ) (κ : ℝ), κ ≠ 0 → (∀ h, 0 < r h) →
 152        (∀ h, r (-h) = r h) →
 153          ¬ (∀ h, 0 < |h| → |h| < 1 →
 154              Real.log (r h) / κ = meshGeometricDeficit h)) :=
 155  ⟨decoy_even_function_ne_mesh_geometricDeficit,
 156    fun r κ hκ hpos heven =>
 157      decoy_log_even_ratio_over_kappa_ne_starDeficit r κ hκ hpos heven⟩
 158
 159/-! ## §4. Status (no ledger flag touch) -/
 160
 161structure RecognitionMeshGeometricDeficit4DStatus where
 162  r1Closed : Bool
 163  encodedFreudenthalLiftOpen : Bool
 164  gap1BridgeDerived : Bool
 165
 166def recognitionMeshGeometricDeficit4DStatus :
 167    RecognitionMeshGeometricDeficit4DStatus where
 168  r1Closed := true
 169  encodedFreudenthalLiftOpen := true
 170  gap1BridgeDerived := false
 171
 172theorem recognitionMeshGeometricDeficit4DStatus_flags :
 173    recognitionMeshGeometricDeficit4DStatus.r1Closed = true ∧
 174      recognitionMeshGeometricDeficit4DStatus.encodedFreudenthalLiftOpen =
 175        true ∧
 176        recognitionMeshGeometricDeficit4DStatus.gap1BridgeDerived =
 177          false := by
 178  decide
 179
 180end
 181
 182end RecognitionMeshGeometricDeficit4D
 183end Analysis
 184end Gravity
 185end IndisputableMonolith
 186