IndisputableMonolith.Gravity.SevenGaps.StationarityBridgeClosure

   1import Mathlib
   2import IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore
   3import IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioBridge
   4
   5/-!
   6# Seven Gaps: stationarity-to-bridge closure (the bridge inhabited by derivation)
   7
   8## Status: THEOREM for every named statement in this file (0 sorry, 0 admit,
   90 new axiom, no `native_decide`; `decide` is used only for `Fin 2` literal
  10disequalities, as in `RecognitionRatioBridge`). MODEL for the deficit-source
  11coupling inside `sourcedAction`, exactly as flagged in
  12`HingeStationarityCore`; that constitutive premise is inherited here and
  13named MODEL everywhere it appears.
  14
  15This module closes the loop left OPEN by `RecognitionRatioBridge` (its
  16`derivation_from_stationarity_open` flag): it builds a CONSTRUCTOR,
  17`recognitionRatioBridge_ofStationarity`, that takes the constitutive
  18deficit-source action data (hinge-wise coupling and deficit, channel count,
  19mesh scale, and a structural source-domination bound) and PROVES the
  20`ratio_relation` field from the stationarity theorems of
  21`HingeStationarityCore`. The bridge structure is thereby INHABITED BY
  22DERIVATION: `xRatio` is DEFINED as the exponential of the total strain of
  23the unique global minimizer of the sourced action
  24(`sourcedMinimizer` / `sourced_unique_minimizer`), and the cubic remainder
  25clause is DERIVED from `sourced_ratio_cubic_error` (constant 1/6). No
  26hypothesis of the constructor is the ratio relation or anything equivalent
  27to it; the audit is in the constructor's docstring.
  28
  29LOCKED promotion language (verbatim, per the campaign): the bridge is
  30"derived from an explicit deficit-source constitutive action plus
  31J-stationarity", never "from the bare RecognitionLedger". The J-cost
  32identification inside that phrase is the kernel equation
  33`sourcedAction_eq_jcost_sum`; the deficit-source coupling is the disclosed
  34constitutive MODEL premise, and the kernel-checked kill records of
  35`HingeStationarityCore` (`closedCycle_coboundary_sum_eq_zero`,
  36`budget_implies_ratio_without_stationarity`) prove the bare-ledger route
  37is dead/circular. Accordingly the status flag
  38`derivation_from_bare_ledger` below is `false` and STAYS false.
  39
  40## Contents
  41
  42* **T1** `stationaryRatio_cubic`: the sourced stationary log-ratio obeys the
  43  bridge-shaped cubic bound |log x* - c| <= (n/6) * h^3 whenever the total
  44  source strength c = kappa*delta is dominated by the mesh, |c| <= n*h. The
  45  h-dependence is explicit: the mesh enters ONLY through the domination
  46  hypothesis; the analysis is `sourced_ratio_cubic_error`, reused, not
  47  re-derived. (The curvature-scaled variant |delta(h)| <= C_K h^2, giving
  48  the sharper O(h^6)-content constant, is already
  49  `sourced_ratio_isAdmissible` in `HingeStationarityCore` and is consumed
  50  below, not restated.)
  51* **T2** the nontrivial admissible family. Panel deviation, recorded
  52  honestly: the panel's literal family delta_m = 1/(m+1),
  53  h_m = |kappa|/(n(m+1)) has delta LINEAR in h (kappa*delta/n = h up to
  54  sign), and the codebase's `RecognitionRatioFamily.IsAdmissible` predicate
  55  hard-codes the curvature conjunct |delta(h)| <= C_K h^2, which a linear
  56  family violates for every constant as h -> 0. That incompatibility is
  57  itself kernel-checked here (`linear_deficit_family_not_isAdmissible`, a
  58  kill record for the literal form). The correctly-typed analogue in this
  59  framework is the QUADRATIC-deficit family delta(h) = (n/kappa) h^2 (so
  60  kappa*delta/n = h^2), `quadraticSourceFamily`: it is genuinely nontrivial
  61  (`quadraticSourceFamily_deficit_ne_zero`,
  62  `quadraticSourceFamily_logRatio_pos`) and satisfies `IsAdmissible` with
  63  UNIFORM constants C_K = n/|kappa|, C_R = n*h0^3/6, constants outside h
  64  (`quadraticSourceFamily_isAdmissible`, via `sourced_ratio_isAdmissible`).
  65  So the derivation covers a genuine h -> 0 family, not a single point.
  66* **T3** `recognitionRatioBridge_ofStationarity`: the headline constructor.
  67  Hypotheses: channel count n >= 1, mesh scale h > 0, and the structural
  68  source-domination bound |kappa sigma * delta sigma| <= n*h at every
  69  hinge. NOT hypotheses: the ratio relation, the value of xRatio, or any
  70  bound on log xRatio. Fields: xRatio sigma := exp(n * arsinh(kappa sigma *
  71  delta sigma / n)) (the exponential of the minimizer's total strain,
  72  `ofStationarity_log_xRatio_eq_minimizer_strain` +
  73  `ofStationarity_minimizer_grounding`); remBound := n/6, the explicit
  74  constant inherited from the 1/6 of `sourced_ratio_cubic_error`;
  75  ratio_relation := proved, by `stationaryRatio_cubic`.
  76* **T4** non-vacuity: `concreteStationarityBridge`, the constructor
  77  instantiated at n = 4, kappa = 1, mesh h = 1/8 (the panel's h_m at m = 1)
  78  on two hinges with SIGNED deficits +1/16 and -1/16 (the quadratic-family
  79  magnitude (n/kappa) h^2 = 1/16 at that mesh, with the sign split of
  80  `ratioBridge_admits_negative_deficit`); every side condition is
  81  discharged by `norm_num`/`decide`. The instance has a strictly negative
  82  deficit at hinge 1 and correspondingly signed log ratios
  83  (`concreteStationarityBridge_nonvacuous`,
  84  `concreteStationarityBridge_logRatio_signed`), so nothing is vacuous.
  85* **T5** status flags: `constitutive_stationarity_bridge_closed := true`,
  86  grounded in the constructor plus the T2 family theorem;
  87  `derivation_from_bare_ledger := false`, which STAYS false (the coupling
  88  is the disclosed constitutive MODEL premise; the bare-ledger route is
  89  killed in `HingeStationarityCore`). NOTE: this module flips NO flag in
  90  `FullTheoryLedger`; whether and how the campaign ledger records this
  91  closure is the conductor's decision, not this module's.
  92
  93## Honest tiers
  94
  95* **THEOREM**: `stationaryRatio_cubic`, `stationaryLogRatio_total_strain`,
  96  `recognitionRatioBridge_ofStationarity` (the constructor itself: its
  97  `ratio_relation` field carries a kernel-checked proof term),
  98  `ofStationarity_xRatio_def`, `ofStationarity_log_xRatio`,
  99  `ofStationarity_log_xRatio_eq_minimizer_strain`,
 100  `ofStationarity_minimizer_grounding`, `ofStationarity_log_xRatio_pos`,
 101  `ofStationarity_log_xRatio_neg`, `linear_deficit_family_not_isAdmissible`,
 102  `quadraticSourceFamily_isAdmissible`,
 103  `quadraticSourceFamily_deficit_ne_zero`,
 104  `quadraticSourceFamily_logRatio_pos`,
 105  `quadraticSourceFamily_source_dominated`,
 106  `concreteStationarityBridge_nonvacuous`,
 107  `concreteStationarityBridge_logRatio_signed`.
 108* **MODEL**: the deficit-source coupling -(kappa*delta/n) * sum_i t_i inside
 109  `sourcedAction` (inherited from `HingeStationarityCore`). Every bridge
 110  produced by the constructor is therefore derived from an explicit
 111  deficit-source constitutive action plus J-stationarity, never from the
 112  bare RecognitionLedger.
 113
 114## Remaining gap (recorded, not hidden)
 115
 116The h -> 0 family content is carried by
 117`RecognitionRatioFamily.IsAdmissible` (uniform constants over (0, h0)),
 118closed here for the quadratic-deficit family. A mesh-INDEXED tower of
 119bridge STRUCTURES (one `RecognitionRatioBridge` per h with a shared
 120remainder constant, i.e. lane 2's full asymptotic object) is not built in
 121this file; the constructor applies at each fixed mesh and the family
 122theorem supplies the uniform constants, but the packaging of the tower is
 123left to lane 2.
 124-/
 125
 126namespace IndisputableMonolith
 127namespace Gravity
 128namespace SevenGaps
 129
 130/-! ## §1. T1: the stationary log-ratio in bridge-shaped form -/
 131
 132/-- **THEOREM.** The total strain of the unique sourced minimizer
 133(`sourcedMinimizer`, t_i = arsinh(c/n)) is n * arsinh(c/n): the quantity
 134whose exponential the constructor uses as xRatio. This is the kernel link
 135between "xRatio is defined from the minimizer" and the closed-form
 136expression the cubic bound is stated about. -/
 137theorem stationaryLogRatio_total_strain (n : ℕ) (c : ℝ) :
 138    ∑ i, sourcedMinimizer n c i = (n : ℝ) * Real.arsinh (c / n) := by
 139  simp only [sourcedMinimizer]
 140  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 141
 142/-- **THEOREM (T1, the bridge-shaped cubic bound).** If the total source
 143strength c = kappa*delta is dominated by the mesh, |c| <= n*h, then the
 144sourced stationary log-ratio log x* = n * arsinh(c/n) (the log of the
 145exponential of the minimizer's total strain) matches c up to the
 146bridge-shaped cubic remainder:
 147
 148  |log x* - c| <= (n/6) * h^3.
 149
 150The h-dependence is EXPLICIT: h enters only through the domination
 151hypothesis, and the constant n/6 is inherited from the 1/6 of
 152`sourced_ratio_cubic_error` via |c|^3/(6 n^2) <= (n h)^3/(6 n^2)
 153= (n/6) h^3. The analysis is reused from `HingeStationarityCore`, not
 154re-derived. (No 0 <= h hypothesis is taken: it is implied by the
 155domination hypothesis, since 0 <= |c| <= n*h and n >= 1.) -/
 156theorem stationaryRatio_cubic (n : ℕ) (hn : 1 ≤ n) (c h : ℝ)
 157    (hdom : |c| ≤ (n : ℝ) * h) :
 158    |Real.log (Real.exp ((n : ℝ) * Real.arsinh (c / n))) - c|
 159      ≤ (n : ℝ) / 6 * h ^ 3 := by
 160  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 161  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
 162  rw [Real.log_exp]
 163  have hcube : |c| ^ 3 ≤ ((n : ℝ) * h) ^ 3 :=
 164    pow_le_pow_left₀ (abs_nonneg c) hdom 3
 165  have hden : (0 : ℝ) ≤ (6 * (n : ℝ) ^ 2)⁻¹ := by positivity
 166  calc |(n : ℝ) * Real.arsinh (c / n) - c|
 167      ≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := sourced_ratio_cubic_error n hn c
 168    _ ≤ ((n : ℝ) * h) ^ 3 / (6 * (n : ℝ) ^ 2) := by
 169        rw [div_eq_mul_inv, div_eq_mul_inv]
 170        exact mul_le_mul_of_nonneg_right hcube hden
 171    _ = (n : ℝ) / 6 * h ^ 3 := by
 172        field_simp
 173
 174/-! ## §2. T3: the constructor (the bridge inhabited by derivation) -/
 175
 176/-- **THEOREM-tier constructor (T3, the headline).** Builds a
 177`RecognitionRatioBridge` from the constitutive deficit-source action data,
 178PROVING the `ratio_relation` field from J-stationarity.
 179
 180Hypothesis audit (every hypothesis is structural; NONE is the ratio
 181relation or equivalent to it):
 182* `hn : 1 ≤ n` — at least one recognition channel (positivity side
 183  condition of `sourced_ratio_cubic_error`).
 184* `hh : 0 < h` — positive mesh scale (the structure's own
 185  `meshScale_pos` field).
 186* `hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ n * h` — source domination: the
 187  total source strength at each hinge is bounded by the mesh budget n*h.
 188  This bounds the INPUT data (coupling times deficit); it says nothing
 189  about xRatio, log xRatio, or the remainder, so it cannot smuggle the
 190  conclusion.
 191
 192Fields produced BY DERIVATION:
 193* `xRatio σ := exp(n * arsinh(kappa σ * geomDeficit σ / n))` — DEFINED as
 194  the exponential of the total strain of the unique global minimizer of
 195  the sourced action `sourcedAction n (kappa σ * geomDeficit σ)`
 196  (`sourcedMinimizer`; uniqueness and global minimality are
 197  `sourced_unique_minimizer`, re-exported for this bridge as
 198  `ofStationarity_minimizer_grounding`).
 199* `remBound := n / 6` — the explicit constant inherited from the 1/6 of
 200  `sourced_ratio_cubic_error`.
 201* `ratio_relation` — PROVED, by `stationaryRatio_cubic`; not passed in.
 202
 203MODEL disclosure: the sourced action's coupling term is the explicit
 204deficit-source constitutive choice of `HingeStationarityCore`. Every
 205bridge this constructor produces is derived from an explicit
 206deficit-source constitutive action plus J-stationarity, never from the
 207bare RecognitionLedger. -/
 208noncomputable def recognitionRatioBridge_ofStationarity {H : Type*}
 209    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 210    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) :
 211    RecognitionRatioBridge H where
 212  xRatio := fun σ =>
 213    Real.exp ((n : ℝ) * Real.arsinh (kappa σ * geomDeficit σ / n))
 214  xRatio_pos := fun _ => Real.exp_pos _
 215  kappa := kappa
 216  geometricDeficit := geomDeficit
 217  meshScale := h
 218  meshScale_pos := hh
 219  remBound := (n : ℝ) / 6
 220  remBound_nonneg := by positivity
 221  ratio_relation := fun σ =>
 222    stationaryRatio_cubic n hn (kappa σ * geomDeficit σ) h (hdom σ)
 223
 224/-- **THEOREM (definitional transparency of the constructor's ratio).**
 225xRatio is the exponential of n * arsinh(kappa*delta/n); recorded as an
 226equation so downstream proofs need not unfold the constructor. -/
 227theorem ofStationarity_xRatio_def {H : Type*}
 228    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 229    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H) :
 230    (recognitionRatioBridge_ofStationarity n hn kappa geomDeficit h hh
 231        hdom).xRatio σ
 232      = Real.exp ((n : ℝ)
 233          * Real.arsinh (kappa σ * geomDeficit σ / n)) := rfl
 234
 235/-- **THEOREM.** The log of the constructed ratio is exactly
 236n * arsinh(kappa*delta/n): the constructed bridge's log ratio is the
 237closed-form stationary value, with NO remainder at this level (the cubic
 238remainder lives between this value and kappa*delta). -/
 239theorem ofStationarity_log_xRatio {H : Type*}
 240    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 241    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H) :
 242    Real.log ((recognitionRatioBridge_ofStationarity n hn kappa geomDeficit
 243        h hh hdom).xRatio σ)
 244      = (n : ℝ) * Real.arsinh (kappa σ * geomDeficit σ / n) := by
 245  rw [ofStationarity_xRatio_def, Real.log_exp]
 246
 247/-- **THEOREM (the derivation receipt).** The log of the constructed ratio
 248IS the total strain of the sourced minimizer with source
 249c = kappa σ * delta σ: this is the sense in which xRatio is defined FROM
 250the stationary point of the constitutive action, not posited. -/
 251theorem ofStationarity_log_xRatio_eq_minimizer_strain {H : Type*}
 252    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 253    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H) :
 254    Real.log ((recognitionRatioBridge_ofStationarity n hn kappa geomDeficit
 255        h hh hdom).xRatio σ)
 256      = ∑ i, sourcedMinimizer n (kappa σ * geomDeficit σ) i := by
 257  rw [ofStationarity_log_xRatio n hn kappa geomDeficit h hh hdom σ]
 258  exact (stationaryLogRatio_total_strain n (kappa σ * geomDeficit σ)).symm
 259
 260/-- **THEOREM (stationarity grounding, re-export of
 261`sourced_unique_minimizer` for the constructed bridge).** The
 262configuration whose total strain the constructed bridge exponentiates is
 263the GLOBAL minimizer of the sourced action at each hinge, and it is the
 264UNIQUE minimizer. So the bridge's ratio field is pinned by J-stationarity
 265of the constitutive action: no other configuration could have produced
 266it. -/
 267theorem ofStationarity_minimizer_grounding {H : Type*}
 268    (n : ℕ) (kappa geomDeficit : H → ℝ) (σ : H) (t : Fin n → ℝ) :
 269    sourcedAction n (kappa σ * geomDeficit σ)
 270        (sourcedMinimizer n (kappa σ * geomDeficit σ))
 271      ≤ sourcedAction n (kappa σ * geomDeficit σ) t ∧
 272      (sourcedAction n (kappa σ * geomDeficit σ) t
 273          = sourcedAction n (kappa σ * geomDeficit σ)
 274              (sourcedMinimizer n (kappa σ * geomDeficit σ)) →
 275        t = sourcedMinimizer n (kappa σ * geomDeficit σ)) :=
 276  sourced_unique_minimizer n (kappa σ * geomDeficit σ) t
 277
 278/-- **THEOREM (signed ratio, positive branch).** Where the source
 279kappa σ * delta σ is positive, the constructed bridge's log ratio is
 280strictly positive: the derivation transports the SIGN of the deficit into
 281log x, exactly the signed information the ledger-deficit no-gos cannot
 282carry (`ratioBridge_separates_deficit_observables`). -/
 283theorem ofStationarity_log_xRatio_pos {H : Type*}
 284    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 285    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H)
 286    (hpos : 0 < kappa σ * geomDeficit σ) :
 287    0 < Real.log ((recognitionRatioBridge_ofStationarity n hn kappa
 288        geomDeficit h hh hdom).xRatio σ) := by
 289  rw [ofStationarity_log_xRatio n hn kappa geomDeficit h hh hdom σ]
 290  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 291  exact mul_pos hn0 (Real.arsinh_pos_iff.mpr (div_pos hpos hn0))
 292
 293/-- **THEOREM (signed ratio, negative branch).** Where the source is
 294negative, the constructed log ratio is strictly negative. -/
 295theorem ofStationarity_log_xRatio_neg {H : Type*}
 296    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
 297    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H)
 298    (hneg : kappa σ * geomDeficit σ < 0) :
 299    Real.log ((recognitionRatioBridge_ofStationarity n hn kappa geomDeficit
 300        h hh hdom).xRatio σ) < 0 := by
 301  rw [ofStationarity_log_xRatio n hn kappa geomDeficit h hh hdom σ]
 302  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 303  exact mul_neg_of_pos_of_neg hn0
 304    (Real.arsinh_neg_iff.mpr (div_neg_of_neg_of_pos hneg hn0))
 305
 306/-! ## §3. T2: the nontrivial uniform small-h family
 307
 308Panel deviation, kernel-checked: the panel's literal family
 309delta_m = 1/(m+1), h_m = |kappa|/(n(m+1)) has delta LINEAR in the mesh
 310(kappa*delta/n = h up to sign). The codebase's admissibility predicate
 311`RecognitionRatioFamily.IsAdmissible` hard-codes the curvature conjunct
 312|delta(h)| <= C_K h^2, which a linear-deficit family violates for EVERY
 313choice of constants once h is small enough. §3 first records that
 314incompatibility as a kill record, then closes T2 with the correctly-typed
 315analogue: the quadratic-deficit family delta(h) = (n/kappa) h^2, whose
 316source satisfies kappa*delta(h)/n = h^2. -/
 317
 318/-- **THEOREM (kill record for the panel's literal linear family).** For
 319every n >= 1, kappa ≠ 0, h0 > 0 and EVERY pair of constants (C_K, C_R),
 320the linear-deficit sourced family delta(h) = (n/kappa) * h (the
 321mesh-indexed form of the panel's delta_m = 1/(m+1), h_m = |kappa|/(n(m+1)),
 322which has kappa*delta/n = h) is NOT admissible: the curvature conjunct
 323|delta(h)| <= C_K h^2 of `RecognitionRatioFamily.IsAdmissible` fails at
 324small h because a linear deficit cannot be dominated by h^2 uniformly.
 325This is why T2 is closed with the quadratic-deficit family below; the
 326deviation from the panel's literal spec is forced by the predicate's
 327curvature conjunct, and this theorem is the receipt. -/
 328theorem linear_deficit_family_not_isAdmissible (n : ℕ) (hn : 1 ≤ n)
 329    (h₀ kappa C_K C_R : ℝ) (hh₀ : 0 < h₀) (hκ : kappa ≠ 0) :
 330    ¬ (sourcedRatioFamily n kappa
 331        (fun h => (n : ℝ) / kappa * h)).IsAdmissible h₀ kappa C_K C_R := by
 332  intro hadm
 333  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 334  have hk : 0 < |kappa| := abs_pos.mpr hκ
 335  set M := max C_K 0 with hMdef
 336  have hM0 : 0 ≤ M := le_max_right _ _
 337  have hden : 0 < |kappa| * (M + 1) := by positivity
 338  set h := min (h₀ / 2) ((n : ℝ) / (|kappa| * (M + 1))) with hdef
 339  have hhpos : 0 < h := lt_min (by linarith) (div_pos hn0 hden)
 340  have hhlt : h < h₀ := lt_of_le_of_lt (min_le_left _ _) (by linarith)
 341  obtain ⟨hcurv, _⟩ := hadm h ⟨hhpos, hhlt⟩
 342  have hcurv' : (n : ℝ) / |kappa| * h ≤ C_K * h ^ 2 := by
 343    have hc : |(n : ℝ) / kappa * h| ≤ C_K * h ^ 2 := hcurv
 344    rw [abs_mul, abs_div, abs_of_pos hn0, abs_of_pos hhpos] at hc
 345    exact hc
 346  have hCM : C_K * h ^ 2 ≤ M * h ^ 2 :=
 347    mul_le_mul_of_nonneg_right (le_max_left _ _) (sq_nonneg h)
 348  have e1 : (n : ℝ) * h ≤ |kappa| * M * h ^ 2 := by
 349    calc (n : ℝ) * h = |kappa| * ((n : ℝ) / |kappa| * h) := by
 350          field_simp
 351      _ ≤ |kappa| * (M * h ^ 2) :=
 352          mul_le_mul_of_nonneg_left (le_trans hcurv' hCM) hk.le
 353      _ = |kappa| * M * h ^ 2 := by ring
 354  have e2 : h * (|kappa| * (M + 1)) ≤ (n : ℝ) := by
 355    have hmin : h ≤ (n : ℝ) / (|kappa| * (M + 1)) := by
 356      rw [hdef]
 357      exact min_le_right _ _
 358    exact (le_div_iff₀ hden).mp hmin
 359  have e3 : h * (|kappa| * (M + 1)) * (M * h) ≤ (n : ℝ) * (M * h) :=
 360    mul_le_mul_of_nonneg_right e2 (mul_nonneg hM0 hhpos.le)
 361  have e4 : (n : ℝ) * h * (M + 1) ≤ |kappa| * M * h ^ 2 * (M + 1) :=
 362    mul_le_mul_of_nonneg_right e1 (by linarith)
 363  have hnh : 0 < (n : ℝ) * h := mul_pos hn0 hhpos
 364  nlinarith [e3, e4, hnh]
 365
 366/-- The quadratic-deficit sourced family (the correctly-typed T2 witness):
 367delta(h) = (n/kappa) * h^2, so the per-channel source is
 368kappa * delta(h) / n = h^2 and the ratio is the sourced stationary value
 369x(h) = exp(n * arsinh(h^2)). Nontrivial for kappa ≠ 0, h ≠ 0
 370(`quadraticSourceFamily_deficit_ne_zero`,
 371`quadraticSourceFamily_logRatio_pos`). -/
 372noncomputable def quadraticSourceFamily (n : ℕ) (kappa : ℝ) :
 373    RecognitionRatioFamily :=
 374  sourcedRatioFamily n kappa (fun h => (n : ℝ) / kappa * h ^ 2)
 375
 376/-- **THEOREM (T2, uniform admissibility of the quadratic family).** For
 377kappa ≠ 0 the quadratic-deficit family is admissible on (0, h0) with the
 378UNIFORM constants C_K = n/|kappa| and C_R = n * h0^3 / 6: both constants
 379sit OUTSIDE the mesh scale, per the admissibility predicate, so the
 380derivation covers a genuine h -> 0 family, not a single point. Proof:
 381`sourced_ratio_isAdmissible` (reused, not re-derived) with the curvature
 382bound an exact equality |delta(h)| = (n/|kappa|) h^2, followed by the
 383constant simplification |kappa|^3 (n/|kappa|)^3 h0^3/(6 n^2)
 384= n h0^3/6. (As in `sourced_ratio_isAdmissible`: for h0 <= 0 the predicate
 385is vacuously true; the statement carries content exactly when 0 < h0.) -/
 386theorem quadraticSourceFamily_isAdmissible (n : ℕ) (hn : 1 ≤ n)
 387    (h₀ kappa : ℝ) (hκ : kappa ≠ 0) :
 388    (quadraticSourceFamily n kappa).IsAdmissible h₀ kappa
 389      ((n : ℝ) / |kappa|) ((n : ℝ) * h₀ ^ 3 / 6) := by
 390  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 391  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
 392  have hκ' : |kappa| ≠ 0 := abs_ne_zero.mpr hκ
 393  have hδ : ∀ h ∈ Set.Ioo (0 : ℝ) h₀,
 394      |(n : ℝ) / kappa * h ^ 2| ≤ (n : ℝ) / |kappa| * h ^ 2 := by
 395    intro h _
 396    rw [abs_mul, abs_div, abs_of_pos hn0, abs_of_nonneg (sq_nonneg h)]
 397  have hbase := sourced_ratio_isAdmissible n hn h₀ kappa
 398    ((n : ℝ) / |kappa|) (fun h => (n : ℝ) / kappa * h ^ 2) hδ
 399  have hconst : |kappa| ^ 3 * ((n : ℝ) / |kappa|) ^ 3 * h₀ ^ 3
 400      / (6 * (n : ℝ) ^ 2) = (n : ℝ) * h₀ ^ 3 / 6 := by
 401    field_simp
 402  rw [← hconst]
 403  exact hbase
 404
 405/-- **THEOREM (nontriviality of the family: nonzero deficit).** For
 406kappa ≠ 0 and every nonzero mesh h, the quadratic family's deficit is
 407nonzero: the admissibility above is about a genuinely sourced family, not
 408the trivial delta = 0 one. -/
 409theorem quadraticSourceFamily_deficit_ne_zero (n : ℕ) (hn : 1 ≤ n)
 410    (kappa h : ℝ) (hκ : kappa ≠ 0) (hh : h ≠ 0) :
 411    (quadraticSourceFamily n kappa).deficit h ≠ 0 := by
 412  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 413  show (n : ℝ) / kappa * h ^ 2 ≠ 0
 414  exact mul_ne_zero (div_ne_zero (ne_of_gt hn0) hκ) (pow_ne_zero 2 hh)
 415
 416/-- **THEOREM (nontriviality of the family: nonzero log ratio).** For
 417kappa ≠ 0 and every nonzero mesh h, the family's stationary log ratio
 418log x(h) = n * arsinh(h^2) is strictly positive: the bridge relation the
 419admissibility certifies is a relation between genuinely nonzero
 420quantities. -/
 421theorem quadraticSourceFamily_logRatio_pos (n : ℕ) (hn : 1 ≤ n)
 422    (kappa h : ℝ) (hκ : kappa ≠ 0) (hh : h ≠ 0) :
 423    0 < Real.log ((quadraticSourceFamily n kappa).ratio h) := by
 424  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 425  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
 426  show 0 < Real.log (Real.exp
 427    ((n : ℝ) * Real.arsinh (kappa * ((n : ℝ) / kappa * h ^ 2) / n)))
 428  rw [Real.log_exp]
 429  have harg : kappa * ((n : ℝ) / kappa * h ^ 2) / n = h ^ 2 := by
 430    field_simp
 431  rw [harg]
 432  have hh2 : 0 < h ^ 2 :=
 433    lt_of_le_of_ne (sq_nonneg h) (Ne.symm (pow_ne_zero 2 hh))
 434  exact mul_pos hn0 (Real.arsinh_pos_iff.mpr hh2)
 435
 436/-- **THEOREM (family members feed the constructor).** For every mesh
 4370 < h <= 1 the quadratic family's source obeys the constructor's
 438domination side condition |kappa * delta(h)| <= n*h (since
 439|kappa * delta(h)| = n h^2 <= n h). So each family member is directly a
 440`recognitionRatioBridge_ofStationarity` input: the uniform-family
 441admissibility (T2) and the bridge-by-derivation construction (T3) cover
 442the same objects. -/
 443theorem quadraticSourceFamily_source_dominated (n : ℕ) (hn : 1 ≤ n)
 444    (kappa h : ℝ) (hκ : kappa ≠ 0) (hh0 : 0 < h) (hh1 : h ≤ 1) :
 445    |kappa * (quadraticSourceFamily n kappa).deficit h| ≤ (n : ℝ) * h := by
 446  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
 447  show |kappa * ((n : ℝ) / kappa * h ^ 2)| ≤ (n : ℝ) * h
 448  have heq : kappa * ((n : ℝ) / kappa * h ^ 2) = (n : ℝ) * h ^ 2 := by
 449    field_simp
 450  rw [heq, abs_of_nonneg (by positivity : (0 : ℝ) ≤ (n : ℝ) * h ^ 2)]
 451  have hsq : h ^ 2 ≤ h := by nlinarith [hh0, hh1]
 452  exact mul_le_mul_of_nonneg_left hsq hn0.le
 453
 454/-! ## §4. T4: the concrete non-vacuity instance
 455
 456The constructor instantiated at fully concrete data: n = 4 channels,
 457kappa = 1, mesh h = 1/8 (the panel's h_m = |kappa|/(n(m+1)) at m = 1), on
 458two hinges carrying SIGNED deficits +1/16 and -1/16. The magnitude 1/16 is
 459the quadratic family's deficit (n/kappa) h^2 = 4 * (1/8)^2 at that mesh;
 460the sign split is the two-hinge pattern of
 461`ratioBridge_admits_negative_deficit`, so the instance exhibits exactly
 462the signed-deficit non-vacuity the bridge modules expect. All side
 463conditions are discharged by `norm_num` (plus `decide` for the Fin 2
 464literal disequality). -/
 465
 466/-- **THEOREM (concrete source domination).** |1 * (±1/16)| = 1/16
 467<= 4 * (1/8) = 1/2: the constructor's only substantive side condition,
 468checked by `norm_num` at the concrete data. -/
 469theorem concreteBridge_hdom : ∀ σ : Fin 2,
 470    |(1 : ℝ) * (if σ = 0 then (1 : ℝ) / 16 else -(1 / 16))|
 471      ≤ ((4 : ℕ) : ℝ) * (1 / 8) := by
 472  intro σ
 473  by_cases hσ : σ = 0
 474  · rw [if_pos hσ, one_mul,
 475      abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 16)]
 476    norm_num
 477  · rw [if_neg hσ, one_mul, abs_neg,
 478      abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 16)]
 479    norm_num
 480
 481/-- **The concrete bridge instance (T4).** The constructor at n = 4,
 482kappa = 1, h = 1/8, deficits +1/16 and -1/16 on two hinges: an actual
 483`RecognitionRatioBridge (Fin 2)` inhabited BY DERIVATION, with every
 484hypothesis discharged numerically. Its ratio_relation field is the proof
 485produced by `stationaryRatio_cubic`; nothing was assumed. -/
 486noncomputable def concreteStationarityBridge : RecognitionRatioBridge (Fin 2) :=
 487  recognitionRatioBridge_ofStationarity 4 (by norm_num)
 488    (fun _ => 1) (fun σ => if σ = 0 then (1 : ℝ) / 16 else -(1 / 16))
 489    (1 / 8) (by norm_num) concreteBridge_hdom
 490
 491/-- **THEOREM (T4 non-vacuity record).** The concrete instance has: the
 492prescribed signed deficits (+1/16 at hinge 0, -1/16 at hinge 1), a
 493STRICTLY NEGATIVE deficit at hinge 1 (the signed-deficit non-vacuity of
 494`ratioBridge_admits_negative_deficit`), mesh 1/8, unit coupling, and the
 495derived remainder constant remBound = 4/6 = 2/3 inherited from the cubic
 496error lemma. (Uses `decide` only for the Fin 2 literal disequality
 4971 ≠ 0, as in `RecognitionRatioBridge`.) -/
 498theorem concreteStationarityBridge_nonvacuous :
 499    concreteStationarityBridge.geometricDeficit 0 = 1 / 16 ∧
 500    concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) ∧
 501    concreteStationarityBridge.geometricDeficit 1 < 0 ∧
 502    concreteStationarityBridge.meshScale = 1 / 8 ∧
 503    concreteStationarityBridge.remBound = 2 / 3 ∧
 504    (∀ σ, concreteStationarityBridge.kappa σ = 1) := by
 505  have h0 : concreteStationarityBridge.geometricDeficit 0 = 1 / 16 := by
 506    show (if (0 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = 1 / 16
 507    rw [if_pos rfl]
 508  have h1 : concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) := by
 509    show (if (1 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = -(1 / 16)
 510    have h10 : ¬((1 : Fin 2) = 0) := by decide
 511    rw [if_neg h10]
 512  refine ⟨h0, h1, ?_, rfl, ?_, fun _ => rfl⟩
 513  · rw [h1]
 514    norm_num
 515  · show ((4 : ℕ) : ℝ) / 6 = 2 / 3
 516    norm_num
 517
 518/-- **THEOREM (T4, signed log ratios).** The concrete instance's log
 519ratios carry the deficit signs: log x_0 > 0 (source +1/16) and
 520log x_1 < 0 (source -1/16). The derived bridge genuinely stores signed
 521information in log x, which the ledger-deficit observables cannot carry
 522(`ratioBridge_separates_deficit_observables`); at concrete numbers this
 523non-vacuity is fully discharged. -/
 524theorem concreteStationarityBridge_logRatio_signed :
 525    0 < Real.log (concreteStationarityBridge.xRatio 0) ∧
 526      Real.log (concreteStationarityBridge.xRatio 1) < 0 := by
 527  constructor
 528  · refine ofStationarity_log_xRatio_pos 4 (by norm_num) (fun _ => 1)
 529      (fun σ => if σ = 0 then (1 : ℝ) / 16 else -(1 / 16)) (1 / 8)
 530      (by norm_num) concreteBridge_hdom 0 ?_
 531    show (0 : ℝ) < 1 * (if (0 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16))
 532    rw [if_pos rfl]
 533    norm_num
 534  · refine ofStationarity_log_xRatio_neg 4 (by norm_num) (fun _ => 1)
 535      (fun σ => if σ = 0 then (1 : ℝ) / 16 else -(1 / 16)) (1 / 8)
 536      (by norm_num) concreteBridge_hdom 1 ?_
 537    show (1 : ℝ) * (if (1 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) < 0
 538    have h10 : ¬((1 : Fin 2) = 0) := by decide
 539    rw [if_neg h10]
 540    norm_num
 541
 542/-! ## §5. T5: status flags (documentation, not mathematics)
 543
 544NOTE for the conductor: this module flips NO flag in `FullTheoryLedger`;
 545whether and how the campaign ledger records this closure is the
 546conductor's decision. -/
 547
 548/-- Status flags for the stationarity-to-bridge closure (documentation
 549record; the mathematics lives in the theorems above, not in these
 550booleans).
 551
 552* `constitutive_stationarity_bridge_closed = true` is grounded in the
 553  constructor `recognitionRatioBridge_ofStationarity` (which PROVES
 554  `ratio_relation` from `stationaryRatio_cubic`, taking only structural
 555  side conditions) together with the uniform-family theorem
 556  `quadraticSourceFamily_isAdmissible` and the concrete instance
 557  `concreteStationarityBridge`. The bridge is derived from an explicit
 558  deficit-source constitutive action plus J-stationarity, never from the
 559  bare RecognitionLedger.
 560* `derivation_from_bare_ledger = false` STAYS false: the deficit-source
 561  coupling inside `sourcedAction` is the disclosed constitutive MODEL
 562  premise, and the kernel-checked kill records in `HingeStationarityCore`
 563  (`closedCycle_coboundary_sum_eq_zero`,
 564  `budget_implies_ratio_without_stationarity`) prove the bare-ledger
 565  route is circular/dead. -/
 566structure StationarityBridgeClosureStatus where
 567  /-- THEOREM tier (this module): the ratio relation is derived from the
 568  constitutive action plus J-stationarity via the constructor. -/
 569  constitutive_stationarity_bridge_closed : Bool
 570  /-- Permanently false: the coupling is a MODEL premise; the bare-ledger
 571  route is killed in `HingeStationarityCore`. -/
 572  derivation_from_bare_ledger : Bool
 573
 574/-- The canonical status record (documentation, not new mathematics). -/
 575def stationarityBridgeClosureStatus : StationarityBridgeClosureStatus where
 576  constitutive_stationarity_bridge_closed := true
 577  derivation_from_bare_ledger := false
 578
 579/-- Status flags record (rfl-forced; documentation, not new
 580mathematics). -/
 581theorem stationarityBridgeClosureStatus_flags :
 582    stationarityBridgeClosureStatus.constitutive_stationarity_bridge_closed
 583        = true ∧
 584      stationarityBridgeClosureStatus.derivation_from_bare_ledger = false :=
 585  ⟨rfl, rfl⟩
 586
 587end SevenGaps
 588end Gravity
 589end IndisputableMonolith
 590