IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D
   3import IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D
   4import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
   5
   6/-!
   7# Wave B residual R2: hinge kappa with source_dominated admissibility (no xRatio)
   8
   9QG full-completion session, Wave B attack on
  10`TypedResidual_hinge_kappa_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 → ℝ` named from RS / mesh
  16constitutive data such that `|κ σ * δ σ|` admits the
  17`DeficitSourceConstitutiveCoupling.source_dominated` bound shape on a
  18positive `meshScale`. Lean has no `HingeCarrier`; R1 already reshaped the
  19carrier to `ℝ` via `meshGeometricDeficit := starDeficit`
  20(`N-gap1-r1-carrier-reshape`).
  21
  22Honest binding used here:
  23* hinge coupling `meshHingeKappa := fun _ => 1`, the unit coupling of the
  24  banked `concreteStationarityBridge` pattern
  25  (`StationarityBridgeClosure`: `∀ σ, kappa σ = 1`); named constitutive
  26  data, not a free field, and definitionally free of `xRatio` / `Real.log`;
  27* geometric side from R1: `meshGeometricDeficit` (= `starDeficit`);
  28* real admissibility content: prove
  29  `|meshHingeKappa h * meshGeometricDeficit h| ≤ channels * meshScale`
  30  for `channels = 4` (bridge channel count) and `meshScale = π/2 > 0`,
  31  using `|arcsin| ≤ π/2` so `|starDeficit| ≤ 2π`;
  32* mesh context conjoined: `ExactJEqualsTrueReggeHessian` and
  33  `starFlatAngleSum = 2π` (same as R1).
  34
  35Blunt honesty: the kappa *naming* is the banked unit-coupling identification
  36(definitional packaging of `1`). The THEOREM content is the
  37`source_dominated`-shaped inequality against banked star geometry, plus
  38nontriviality (`κ ≠ 0`) and the decoys. Continuum Einstein-scale join
  39(`kappa_einstein` vs hinge-local unit coupling) is left OPEN via
  40`einsteinScaleJoinOpen`.
  41
  42Does **not** flip `gap1_bridge_derived`. Does **not** inhabit
  43`DeficitSourceConstitutiveCoupling` (needs R3 enrichment for signed
  44`sourceStrength`). Does **not** touch R3 / evade
  45`no_bare_ledger_selector_recovers_signed_source`.
  46-/
  47
  48namespace IndisputableMonolith
  49namespace Gravity
  50namespace Analysis
  51namespace RecognitionMeshHingeKappa4D
  52
  53open RecognitionMeshGeometricDeficit4D
  54open RecognitionMeshExactJBridge4D
  55open ReggeHinge4DStarKernel
  56
  57noncomputable section
  58
  59/-! ## §1. Named hinge coupling (no xRatio) -/
  60
  61/-- Mesh hinge coupling: unit coupling of the banked
  62`concreteStationarityBridge` pattern. No `xRatio`, no `Real.log`. -/
  63def meshHingeKappa : ℝ → ℝ :=
  64  fun _ => 1
  65
  66theorem meshHingeKappa_eq_one (h : ℝ) : meshHingeKappa h = 1 := rfl
  67
  68theorem meshHingeKappa_ne_zero (h : ℝ) : meshHingeKappa h ≠ 0 := by
  69  simp [meshHingeKappa]
  70
  71/-! ## §2. Geometric bound feeding source_dominated -/
  72
  73/-- `|arcsin h| ≤ π/2` for every real (Mathlib clamps outside `[-1,1]`). -/
  74theorem abs_arcsin_le_pi_div_two (h : ℝ) :
  75    |Real.arcsin h| ≤ Real.pi / 2 := by
  76  have hle : Real.arcsin h ≤ Real.pi / 2 := Real.arcsin_le_pi_div_two h
  77  have hge : -(Real.pi / 2) ≤ Real.arcsin h := Real.neg_pi_div_two_le_arcsin h
  78  exact abs_le.mpr ⟨hge, hle⟩
  79
  80/-- Banked star deficit is uniformly bounded: `|δ| ≤ 2π`. -/
  81theorem meshGeometricDeficit_abs_le_two_pi (h : ℝ) :
  82    |meshGeometricDeficit h| ≤ 2 * Real.pi := by
  83  rw [meshGeometricDeficit_eq_arcsin, abs_mul,
  84    abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 4)]
  85  have hbound := abs_arcsin_le_pi_div_two h
  86  have h4 : (0 : ℝ) ≤ 4 := by norm_num
  87  calc 4 * |Real.arcsin h|
  88      ≤ 4 * (Real.pi / 2) := mul_le_mul_of_nonneg_left hbound h4
  89    _ = 2 * Real.pi := by ring
  90
  91/-- Bridge channel count used by `concreteStationarityBridge`. -/
  92def meshHingeChannels : ℕ := 4
  93
  94theorem meshHingeChannels_pos : 1 ≤ meshHingeChannels := by
  95  decide
  96
  97/-- Positive mesh scale discharging `source_dominated` against star geometry:
  98`4 * (π/2) = 2π` matches the uniform deficit bound. -/
  99def meshHingeMeshScale : ℝ := Real.pi / 2
 100
 101theorem meshHingeMeshScale_pos : 0 < meshHingeMeshScale := by
 102  unfold meshHingeMeshScale
 103  positivity
 104
 105/-- **THEOREM (real admissibility).** The named unit coupling admits the
 106`DeficitSourceConstitutiveCoupling.source_dominated` bound shape against
 107R1's `meshGeometricDeficit` on a positive mesh scale:
 108`|κ h * δ h| ≤ channels * meshScale` for all carrier points. -/
 109theorem meshHingeKappa_source_dominated :
 110    ∀ h : ℝ,
 111      |meshHingeKappa h * meshGeometricDeficit h|
 112        ≤ (meshHingeChannels : ℝ) * meshHingeMeshScale := by
 113  intro h
 114  rw [meshHingeKappa_eq_one, one_mul]
 115  have hδ := meshGeometricDeficit_abs_le_two_pi h
 116  unfold meshHingeChannels meshHingeMeshScale
 117  -- `|δ| ≤ 2π = 4 * (π/2)`
 118  have hscale : (4 : ℝ) * (Real.pi / 2) = 2 * Real.pi := by ring
 119  rw [← hscale] at hδ
 120  exact hδ
 121
 122/-! ## §3. Typed residual R2 -/
 123
 124/-- **R2.** Hinge kappa identified with source_dominated admissibility
 125(no xRatio).
 126
 127Inhabits the DAG residual under the R1 carrier reshape: `κ` is the banked
 128unit coupling, nontrivial, and `|κ * meshGeometricDeficit|` meets the
 129blocker `source_dominated` shape on `meshHingeMeshScale > 0`, with the
 130exact-J / seed-flat mesh context conjoined. -/
 131def TypedResidual_hinge_kappa_identified : Prop :=
 132  ∃ κ : ℝ → ℝ,
 133    κ = meshHingeKappa ∧
 134      (∀ h : ℝ, κ h ≠ 0) ∧
 135        (∃ (channels : ℕ), 1 ≤ channels ∧
 136          ∃ meshScale : ℝ, 0 < meshScale ∧
 137            ∀ h : ℝ,
 138              |κ h * meshGeometricDeficit h| ≤ (channels : ℝ) * meshScale) ∧
 139          ExactJEqualsTrueReggeHessian ∧
 140            starFlatAngleSum = 2 * Real.pi
 141
 142/-- **THEOREM:** R2 closed. -/
 143theorem typedResidual_hinge_kappa_identified_closed :
 144    TypedResidual_hinge_kappa_identified := by
 145  refine ⟨meshHingeKappa, rfl, meshHingeKappa_ne_zero, ?_,
 146    exactJEqualsTrueReggeHessian_holds, star_flat_angle_sum_two_pi⟩
 147  exact ⟨meshHingeChannels, meshHingeChannels_pos,
 148    meshHingeMeshScale, meshHingeMeshScale_pos,
 149    meshHingeKappa_source_dominated⟩
 150
 151/-- Named alias matching the DAG residual title. -/
 152theorem TypedResidual_hinge_kappa_identified_closed :
 153    TypedResidual_hinge_kappa_identified :=
 154  typedResidual_hinge_kappa_identified_closed
 155
 156/-! ## §4. Decoys / falsifiers (DAG) -/
 157
 158/-- **Decoy:** `κ = 0` everywhere trivializes the source and fails the
 159nontriviality conjunct required by R2. -/
 160theorem decoy_zero_kappa_fails_nontrivial :
 161    ¬ (∀ h : ℝ, (fun _ : ℝ => (0 : ℝ)) h ≠ 0) := by
 162  intro h
 163  exact (h 0) rfl
 164
 165/-- **Decoy:** `κ h := log(r h) / δ h` with even positive ratio (smuggles
 166the recognition ratio into the coupling) cannot equal the named constitutive
 167unit coupling on a punctured interval. Oddness of `meshGeometricDeficit`
 168forces the log-ratio quotient to be odd, while `meshHingeKappa` is the
 169nonzero constant `1`. -/
 170theorem decoy_log_ratio_over_deficit_ne_meshHingeKappa
 171    (r : ℝ → ℝ) (_hr_pos : ∀ h : ℝ, 0 < r h)
 172    (hr_even : ∀ h : ℝ, r (-h) = r h) :
 173    ¬ (∀ h : ℝ, 0 < |h| → |h| < 1 →
 174        Real.log (r h) / meshGeometricDeficit h = meshHingeKappa h) := by
 175  intro hEq
 176  -- Evaluate at a concrete positive deformation in (0,1), e.g. 1/2.
 177  have hpos : (0 : ℝ) < |(1 / 2 : ℝ)| := by norm_num
 178  have hlt : |(1 / 2 : ℝ)| < 1 := by norm_num
 179  have hpos' : (0 : ℝ) < |(-(1 / 2 : ℝ))| := by norm_num
 180  have hlt' : |(-(1 / 2 : ℝ))| < 1 := by norm_num
 181  have heq_pos := hEq (1 / 2) hpos hlt
 182  have heq_neg := hEq (-(1 / 2)) hpos' hlt'
 183  -- Left side at -h equals negation of left side at h (δ odd, r even).
 184  have hδ_odd := meshGeometricDeficit_odd (1 / 2)
 185  have hr := hr_even (1 / 2)
 186  have hneg_side :
 187      Real.log (r (-(1 / 2))) / meshGeometricDeficit (-(1 / 2))
 188        = -(Real.log (r (1 / 2)) / meshGeometricDeficit (1 / 2)) := by
 189    rw [hr, hδ_odd, div_neg]
 190  -- Right side is constantly 1.
 191  have hκ_pos : meshHingeKappa (1 / 2) = 1 := meshHingeKappa_eq_one _
 192  have hκ_neg : meshHingeKappa (-(1 / 2)) = 1 := meshHingeKappa_eq_one _
 193  -- So 1 = lhs(-h) = -lhs(h) = -1, contradiction.
 194  have hlhs_pos :
 195      Real.log (r (1 / 2)) / meshGeometricDeficit (1 / 2) = 1 := by
 196    rw [heq_pos, hκ_pos]
 197  have hlhs_neg :
 198      Real.log (r (-(1 / 2))) / meshGeometricDeficit (-(1 / 2)) = 1 := by
 199    rw [heq_neg, hκ_neg]
 200  rw [hneg_side, hlhs_pos] at hlhs_neg
 201  linarith
 202
 203/-- Package: both DAG decoys. -/
 204theorem adversarial_decoys_hinge_kappa :
 205    (¬ (∀ h : ℝ, (fun _ : ℝ => (0 : ℝ)) h ≠ 0)) ∧
 206      (∀ (r : ℝ → ℝ), (∀ h, 0 < r h) → (∀ h, r (-h) = r h) →
 207        ¬ (∀ h, 0 < |h| → |h| < 1 →
 208            Real.log (r h) / meshGeometricDeficit h = meshHingeKappa h)) :=
 209  ⟨decoy_zero_kappa_fails_nontrivial,
 210    fun r hpos heven =>
 211      decoy_log_ratio_over_deficit_ne_meshHingeKappa r hpos heven⟩
 212
 213/-! ## §5. Status (no ledger flag touch) -/
 214
 215structure RecognitionMeshHingeKappa4DStatus where
 216  r2Closed : Bool
 217  einsteinScaleJoinOpen : Bool
 218  gap1BridgeDerived : Bool
 219
 220def recognitionMeshHingeKappa4DStatus :
 221    RecognitionMeshHingeKappa4DStatus where
 222  r2Closed := true
 223  einsteinScaleJoinOpen := true
 224  gap1BridgeDerived := false
 225
 226theorem recognitionMeshHingeKappa4DStatus_flags :
 227    recognitionMeshHingeKappa4DStatus.r2Closed = true ∧
 228      recognitionMeshHingeKappa4DStatus.einsteinScaleJoinOpen = true ∧
 229        recognitionMeshHingeKappa4DStatus.gap1BridgeDerived = false := by
 230  decide
 231
 232end
 233
 234end RecognitionMeshHingeKappa4D
 235end Analysis
 236end Gravity
 237end IndisputableMonolith
 238