IndisputableMonolith.Gravity.Analysis.RecognitionMeshDualEntryCoupling4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D
   3import IndisputableMonolith.Gravity.Analysis.RecognitionMeshGeometricDeficit4D
   4import IndisputableMonolith.Gravity.Analysis.RecognitionMeshHingeKappa4D
   5
   6/-!
   7# Wave B residual R4: mesh dual-entry DeficitSourceConstitutiveCoupling
   8
   9QG full-completion session, Wave B attack on
  10`TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment` from
  11`plans/QG_WaveB_Gap1_Residual_DAG_Draft_20260721.txt`.
  12
  13Assembles banked R1 (`meshGeometricDeficit`), R2 (`meshHingeKappa` +
  14`source_dominated`), and R3 (`DualEntryStrainState`) into an inhabited
  15`DeficitSourceConstitutiveCoupling ℝ`, then applies the blocker's conditional
  16`recognition_ratio_derived_of_deficit_source_coupling`.
  17
  18## Honesty / scope
  19
  20* Does **not** flip `gap1_bridge_derived`.
  21* Does **not** introduce a ledger-named standalone
  22  `recognition_ratio_derived` Prop binding (that is R5); the theorem here is
  23  the conditional application on the assembled coupling, named
  24  `mesh_recognition_ratio_derived`.
  25* Carrier is the reshaped `H = ℝ` from R1/R2, not an encoded Freudenthal
  26  triangulation (`encodedFreudenthalLiftOpen` remains true upstream).
  27* R0a/R0b validation name-bindings remain open.
  28* Convention: deficit iff debit-leads (`0 < h`), mirror of
  29  `meshGeometricDeficit_regge_convention` (see `N-gap1-r3-convention-pin`).
  30
  31Definitions are free of `xRatio` / `Real.log` / `ratio_relation`; the log
  32appears only in the final derived-ratio theorem statement inherited from
  33the blocker.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Gravity
  38namespace Analysis
  39namespace RecognitionMeshDualEntryCoupling4D
  40
  41open RecognitionDualEntryEnrichment4D
  42open RecognitionMeshGeometricDeficit4D
  43open RecognitionMeshHingeKappa4D
  44open SevenGaps
  45
  46noncomputable section
  47
  48/-! ## §1. Mesh dual-entry enrichment on the deformation carrier -/
  49
  50/-- Dual-entry state on a single mesh channel (`Fin 1`): debit-leads on
  51positive deformation, credit-leads on negative, magnitude
  52`|meshGeometricDeficit h|`. -/
  53noncomputable def meshDualEntry (h : ℝ) : DualEntryStrainState (Fin 1) where
  54  debit := fun _ => if 0 < h then (1 : ℤ) else 0
  55  credit := fun _ => if h < 0 then (1 : ℤ) else 0
  56  mag := fun _ => |meshGeometricDeficit h|
  57  mag_nonneg := fun _ => abs_nonneg _
  58  flux_unit := by
  59    intro _
  60    by_cases hpos : 0 < h
  61    · have hneg : ¬ h < 0 := not_lt.mpr (le_of_lt hpos)
  62      simp [hpos, hneg]
  63    · by_cases hneg : h < 0
  64      · simp [hpos, hneg]
  65      · simp [hpos, hneg]
  66
  67/-- Signed source strength extracted from the mesh dual-entry state. -/
  68noncomputable def meshDualEntrySource (h : ℝ) : ℝ :=
  69  (meshDualEntry h).extract 0
  70
  71/-- **THEOREM.** Extracted dual-entry source equals the R2 constitutive
  72product `κ * δ` (trichotomy on `h`). -/
  73theorem meshDualEntrySource_eq (h : ℝ) :
  74    meshDualEntrySource h =
  75      meshHingeKappa h * meshGeometricDeficit h := by
  76  unfold meshDualEntrySource DualEntryStrainState.extract
  77    DualEntryStrainState.strain DualEntryStrainState.phi meshDualEntry
  78  rw [meshHingeKappa_eq_one, one_mul]
  79  -- Only cell of Fin 1 is 0.
  80  simp only
  81  rcases lt_trichotomy h 0 with hlt | rfl | hgt
  82  · -- h < 0: debit=0, credit=1, phi=-1, strain = -|δ| = δ
  83    have hsign := (meshGeometricDeficit_sign h).2 hlt
  84    have habs : |meshGeometricDeficit h| = -meshGeometricDeficit h :=
  85      abs_of_neg hsign
  86    have hpos : ¬ 0 < h := not_lt.mpr (le_of_lt hlt)
  87    simp [hlt, hpos, habs]
  88  · -- h = 0: flat
  89    simp [meshGeometricDeficit_flat, abs_zero]
  90  · -- 0 < h: debit=1, credit=0, phi=1, strain = |δ| = δ
  91    have hsign := (meshGeometricDeficit_sign h).1 hgt
  92    have habs : |meshGeometricDeficit h| = meshGeometricDeficit h :=
  93      abs_of_pos hsign
  94    have hneg : ¬ h < 0 := not_lt.mpr (le_of_lt hgt)
  95    simp [hgt, hneg, habs]
  96
  97/-! ## §2. Assembled constitutive coupling -/
  98
  99/-- **R4 assembly.** `DeficitSourceConstitutiveCoupling ℝ` from R1–R3:
 100channels/kappa/geometricDeficit/meshScale from banked R1/R2, source from
 101dual-entry extract. Definitionally free of `xRatio` / `Real.log`. -/
 102noncomputable def meshDualEntryCoupling :
 103    DeficitSourceConstitutiveCoupling ℝ where
 104  channels := meshHingeChannels
 105  channels_pos := meshHingeChannels_pos
 106  kappa := meshHingeKappa
 107  geometricDeficit := meshGeometricDeficit
 108  sourceStrength := meshDualEntrySource
 109  source_eq := meshDualEntrySource_eq
 110  meshScale := meshHingeMeshScale
 111  meshScale_pos := meshHingeMeshScale_pos
 112  source_dominated := by
 113    intro σ
 114    rw [meshDualEntrySource_eq σ]
 115    exact meshHingeKappa_source_dominated σ
 116
 117/-- **THEOREM (conditional recognition-ratio on the mesh coupling).**
 118Applies `recognition_ratio_derived_of_deficit_source_coupling` to the
 119assembled dual-entry coupling. This is **not** the ledger-named
 120standalone `recognition_ratio_derived` binding (R5) and does **not** flip
 121`gap1_bridge_derived` (R6 needs R0a+R0b+R5). -/
 122theorem mesh_recognition_ratio_derived (σ : ℝ) :
 123    |Real.log ((ratioBridgeFromDeficitSourceCoupling
 124          meshDualEntryCoupling).xRatio σ)
 125        - meshDualEntryCoupling.kappa σ
 126            * meshDualEntryCoupling.geometricDeficit σ|
 127      ≤ (meshDualEntryCoupling.channels : ℝ) / 6
 128          * meshDualEntryCoupling.meshScale ^ 3 :=
 129  recognition_ratio_derived_of_deficit_source_coupling
 130    meshDualEntryCoupling σ
 131
 132/-! ## §3. Typed residual R4 -/
 133
 134/-- **R4.** Coupling assembled from enrichment + R1/R2 with source_eq and
 135source_dominated, free of xRatio in the premise fields. -/
 136def TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment :
 137    Prop :=
 138  ∃ C : DeficitSourceConstitutiveCoupling ℝ,
 139    C.kappa = meshHingeKappa ∧
 140      C.geometricDeficit = meshGeometricDeficit ∧
 141        C.sourceStrength = meshDualEntrySource ∧
 142          (∀ σ, C.sourceStrength σ = C.kappa σ * C.geometricDeficit σ) ∧
 143            0 < C.meshScale ∧
 144              (∀ σ, |C.sourceStrength σ| ≤ (C.channels : ℝ) * C.meshScale) ∧
 145                1 ≤ C.channels
 146
 147/-- **THEOREM:** R4 closed. -/
 148theorem typedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed :
 149    TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment := by
 150  refine ⟨meshDualEntryCoupling, rfl, rfl, rfl, ?_,
 151    meshDualEntryCoupling.meshScale_pos, ?_, meshDualEntryCoupling.channels_pos⟩
 152  · exact meshDualEntryCoupling.source_eq
 153  · exact meshDualEntryCoupling.source_dominated
 154
 155theorem TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed :
 156    TypedResidual_DeficitSourceConstitutiveCoupling_from_enrichment :=
 157  typedResidual_DeficitSourceConstitutiveCoupling_from_enrichment_closed
 158
 159/-! ## §4. Decoys -/
 160
 161/-- **Decoy 2.** Columnless magnitude-only extract `|δ|` is even in `h` and
 162cannot match the signed mesh geometric deficit on a punctured interval
 163(banked R1 even-function decoy). -/
 164theorem decoy_magnitude_only_ne_mesh_geometricDeficit :
 165    ¬ (∀ h : ℝ, 0 < |h| → |h| < 1 →
 166        |meshGeometricDeficit h| = meshGeometricDeficit h) := by
 167  have heven : ∀ h : ℝ, |meshGeometricDeficit (-h)| = |meshGeometricDeficit h| := by
 168    intro h
 169    rw [meshGeometricDeficit_odd h, abs_neg]
 170  exact decoy_even_function_ne_mesh_geometricDeficit
 171    (fun h => |meshGeometricDeficit h|) heven
 172
 173/-- Package: magnitude-only decoy plus swap-evenness from R3 (decoy 1). -/
 174theorem adversarial_decoys_mesh_dual_entry :
 175    (¬ (∀ h : ℝ, 0 < |h| → |h| < 1 →
 176        |meshGeometricDeficit h| = meshGeometricDeficit h)) ∧
 177      (∀ (f : DualEntryStrainState (Fin 2) → ℝ)
 178          (select : RecognitionLedger.RecognitionLedger (Fin 2) → ℝ),
 179        (∀ E, f E = select E.toBare) →
 180          ∀ E, f E.swap = f E) :=
 181  ⟨decoy_magnitude_only_ne_mesh_geometricDeficit,
 182    fun f select hf E => bare_factorable_is_swap_even f select hf E⟩
 183
 184/-! ## §5. Status (no ledger flag touch) -/
 185
 186structure RecognitionMeshDualEntryCoupling4DStatus where
 187  r4Closed : Bool
 188  recognitionRatioDerivedLedgerBindingOpen : Bool
 189  gap1BridgeDerived : Bool
 190
 191/-- R5 lands the ledger-named binding in
 192`SevenGaps.RecognitionRatioDerived`; this status field records that the
 193R4 module itself does not own that binding (binding lives in R5). -/
 194def recognitionMeshDualEntryCoupling4DStatus :
 195    RecognitionMeshDualEntryCoupling4DStatus where
 196  r4Closed := true
 197  recognitionRatioDerivedLedgerBindingOpen := true
 198  gap1BridgeDerived := false
 199
 200theorem recognitionMeshDualEntryCoupling4DStatus_flags :
 201    recognitionMeshDualEntryCoupling4DStatus.r4Closed = true ∧
 202      recognitionMeshDualEntryCoupling4DStatus.recognitionRatioDerivedLedgerBindingOpen =
 203        true ∧
 204        recognitionMeshDualEntryCoupling4DStatus.gap1BridgeDerived = false := by
 205  decide
 206
 207end
 208
 209end RecognitionMeshDualEntryCoupling4D
 210end Analysis
 211end Gravity
 212end IndisputableMonolith
 213