IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioDerived

   1import IndisputableMonolith.Gravity.Analysis.RecognitionMeshDualEntryCoupling4D
   2import IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioSubstrateBlocker
   3
   4/-!
   5# Wave B residual R5: ledger-named `recognition_ratio_derived`
   6
   7QG full-completion session, Wave B. Packages the R4 inhabited coupling
   8`meshDualEntryCoupling` with the blocker's conditional derivation and the
   9stationarity minimizer receipt under the exact ledger Prop name named by
  10`FullTheoryLedger.FullTheoryBenchmarks.gap1_bridge_derived`.
  11
  12## Honesty / scope
  13
  14* Does **not** flip `gap1_bridge_derived` (R6 needs R0a + R0b + this Prop).
  15* Carrier remains the reshaped `H = ℝ` from R1–R4, not an encoded
  16  Freudenthal triangulation (`encodedFreudenthalLiftOpen` upstream).
  17* The enrichment existential is discharged by the mesh dual-entry family
  18  `meshDualEntry` (R3/R4), not by a bare `RecognitionLedger`.
  19* No field of the premise smuggles `xRatio`; the log appears only in the
  20  derived conclusions inherited from the blocker.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Gravity
  25namespace SevenGaps
  26
  27open Analysis.RecognitionMeshDualEntryCoupling4D
  28open Analysis.RecognitionDualEntryEnrichment4D
  29
  30noncomputable section
  31
  32/-! ## §1. Ledger-named closing Prop (derivation half) -/
  33
  34/-- **Ledger-named Prop (derivation half of `gap1_bridge_derived`).**
  35
  36There exists a dual-entry enrichment and an assembled
  37`DeficitSourceConstitutiveCoupling` equal to the mesh dual-entry coupling,
  38such that (i) the blocker's conditional recognition-ratio inequality holds
  39at every carrier point, and (ii) the log-ratio equals the total strain of
  40the unique sourced J-stationarity minimizer (so `xRatio` is the
  41exponential of that minimizer strain, not a posited field). -/
  42def recognition_ratio_derived : Prop :=
  43  ∃ (E : ℝ → DualEntryStrainState (Fin 1))
  44    (C : DeficitSourceConstitutiveCoupling ℝ),
  45    (∀ h, E h = meshDualEntry h) ∧
  46      C = meshDualEntryCoupling ∧
  47        (∀ σ,
  48          |Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
  49              - C.kappa σ * C.geometricDeficit σ|
  50            ≤ (C.channels : ℝ) / 6 * C.meshScale ^ 3) ∧
  51          (∀ σ,
  52            Real.log ((ratioBridgeFromDeficitSourceCoupling C).xRatio σ)
  53              = ∑ i, sourcedMinimizer C.channels (C.sourceStrength σ) i) ∧
  54            (∀ σ,
  55              (ratioBridgeFromDeficitSourceCoupling C).xRatio σ
  56                = Real.exp
  57                    (∑ i, sourcedMinimizer C.channels
  58                      (C.sourceStrength σ) i))
  59
  60/-- **THEOREM (R5 closed).** The ledger-named Prop is inhabited by the
  61mesh dual-entry coupling: conditional inequality from
  62`recognition_ratio_derived_of_deficit_source_coupling`, minimizer
  63identification from `deficitSourceCoupling_logRatio_eq_minimizer_strain`. -/
  64theorem recognition_ratio_derived_holds : recognition_ratio_derived := by
  65  refine ⟨meshDualEntry, meshDualEntryCoupling, fun _ => rfl, rfl, ?_, ?_, ?_⟩
  66  · intro σ
  67    exact recognition_ratio_derived_of_deficit_source_coupling
  68      meshDualEntryCoupling σ
  69  · intro σ
  70    exact deficitSourceCoupling_logRatio_eq_minimizer_strain
  71      meshDualEntryCoupling σ
  72  · intro σ
  73    have hlog :=
  74      deficitSourceCoupling_logRatio_eq_minimizer_strain meshDualEntryCoupling σ
  75    have hpos :
  76        0 < (ratioBridgeFromDeficitSourceCoupling
  77          meshDualEntryCoupling).xRatio σ :=
  78      (ratioBridgeFromDeficitSourceCoupling meshDualEntryCoupling).xRatio_pos σ
  79    calc (ratioBridgeFromDeficitSourceCoupling meshDualEntryCoupling).xRatio σ
  80        = Real.exp
  81            (Real.log
  82              ((ratioBridgeFromDeficitSourceCoupling
  83                meshDualEntryCoupling).xRatio σ)) :=
  84          (Real.exp_log hpos).symm
  85      _ = Real.exp
  86            (∑ i, sourcedMinimizer meshDualEntryCoupling.channels
  87              (meshDualEntryCoupling.sourceStrength σ) i) := by
  88          rw [hlog]
  89
  90/-- Alias matching the DAG residual name. -/
  91def TypedResidual_recognition_ratio_derived : Prop :=
  92  recognition_ratio_derived
  93
  94theorem typedResidual_recognition_ratio_derived_closed :
  95    TypedResidual_recognition_ratio_derived :=
  96  recognition_ratio_derived_holds
  97
  98theorem TypedResidual_recognition_ratio_derived_closed :
  99    TypedResidual_recognition_ratio_derived :=
 100  typedResidual_recognition_ratio_derived_closed
 101
 102/-! ## §2. Status (no FullTheoryLedger / CampaignLedger flag touch) -/
 103
 104structure RecognitionRatioDerivedStatus where
 105  r5Closed : Bool
 106  gap1BridgeDerived : Bool
 107
 108def recognitionRatioDerivedStatus : RecognitionRatioDerivedStatus where
 109  r5Closed := true
 110  gap1BridgeDerived := false
 111
 112theorem recognitionRatioDerivedStatus_flags :
 113    recognitionRatioDerivedStatus.r5Closed = true ∧
 114      recognitionRatioDerivedStatus.gap1BridgeDerived = false := by
 115  decide
 116
 117end
 118
 119end SevenGaps
 120end Gravity
 121end IndisputableMonolith
 122