Gravity Seven Gaps Stationarity Bridge Closure

/-- Status flags record (rfl-forced; documentation, not new
mathematics). -/
theorem stationarityBridgeClosureStatus_flags :
    stationarityBridgeClosureStatus.constitutive_stationarity_bridge_closed
        = true ∧
      stationarityBridgeClosureStatus.derivation_from_bare_ledger = false :=
  ⟨rfl, rfl⟩

/-- **THEOREM (T1, the bridge-shaped cubic bound).** If the total source
strength c = kappa*delta is dominated by the mesh, |c| <= n*h, then the
sourced stationary log-ratio log x* = n * arsinh(c/n) (the log of the
exponential of the minimizer's total strain) matches c up to the
bridge-shaped cubic remainder:

  |log x* - c| <= (n/6) * h^3.

The h-dependence is EXPLICIT: h enters only through the domination
hypothesis, and the constant n/6 is inherited from the 1/6 of
`sourced_ratio_cubic_error` via |c|^3/(6 n^2) <= (n h)^3/(6 n^2)
= (n/6) h^3. The analysis is reused from `HingeStationarityCore`, not
re-derived. (No 0 <= h hypothesis is taken: it is implied by the
domination hypothesis, since 0 <= |c| <= n*h and n >= 1.) -/
theorem stationaryRatio_cubic (n : ℕ) (hn : 1 ≤ n) (c h : ℝ)
    (hdom : |c| ≤ (n : ℝ) * h) :
    |Real.log (Real.exp ((n : ℝ) * Real.arsinh (c / n))) - c|
      ≤ (n : ℝ) / 6 * h ^ 3 := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  rw [Real.log_exp]
  have hcube : |c| ^ 3 ≤ ((n : ℝ) * h) ^ 3 :=
    pow_le_pow_left₀ (abs_nonneg c) hdom 3
  have hden : (0 : ℝ) ≤ (6 * (n : ℝ) ^ 2)⁻¹ := by positivity
  calc |(n : ℝ) * Real.arsinh (c / n) - c|
      ≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := sourced_ratio_cubic_error n hn c
    _ ≤ ((n : ℝ) * h) ^ 3 / (6 * (n : ℝ) ^ 2) := by
        rw [div_eq_mul_inv, div_eq_mul_inv]
        exact mul_le_mul_of_nonneg_right hcube hden
    _ = (n : ℝ) / 6 * h ^ 3 := by
        field_simp

/-- **THEOREM (kill record for the panel's literal linear family).** For
every n >= 1, kappa ≠ 0, h0 > 0 and EVERY pair of constants (C_K, C_R),
the linear-deficit sourced family delta(h) = (n/kappa) * h (the
mesh-indexed form of the panel's delta_m = 1/(m+1), h_m = |kappa|/(n(m+1)),
which has kappa*delta/n = h) is NOT admissible: the curvature conjunct
|delta(h)| <= C_K h^2 of `RecognitionRatioFamily.IsAdmissible` fails at
small h because a linear deficit cannot be dominated by h^2 uniformly.
This is why T2 is closed with the quadratic-deficit family below; the
deviation from the panel's literal spec is forced by the predicate's
curvature conjunct, and this theorem is the receipt. -/
theorem linear_deficit_family_not_isAdmissible (n : ℕ) (hn : 1 ≤ n)
    (h₀ kappa C_K C_R : ℝ) (hh₀ : 0 < h₀) (hκ : kappa ≠ 0) :
    ¬ (sourcedRatioFamily n kappa
        (fun h => (n : ℝ) / kappa * h)).IsAdmissible h₀ kappa C_K C_R := by
  intro hadm
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hk : 0 < |kappa| := abs_pos.mpr hκ
  set M := max C_K 0 with hMdef
  have hM0 : 0 ≤ M := le_max_right _ _
  have hden : 0 < |kappa| * (M + 1) := by positivity
  set h := min (h₀ / 2) ((n : ℝ) / (|kappa| * (M + 1))) with hdef
  have hhpos : 0 < h := lt_min (by linarith) (div_pos hn0 hden)
  have hhlt : h < h₀ := lt_of_le_of_lt (min_le_left _ _) (by linarith)
  obtain ⟨hcurv, _⟩ := hadm h ⟨hhpos, hhlt⟩
  have hcurv' : (n : ℝ) / |kappa| * h ≤ C_K * h ^ 2 := by
    have hc : |(n : ℝ) / kappa * h| ≤ C_K * h ^ 2 := hcurv
    rw [abs_mul, abs_div, abs_of_pos hn0, abs_of_pos hhpos] at hc
    exact hc
  have hCM : C_K * h ^ 2 ≤ M * h ^ 2 :=
    mul_le_mul_of_nonneg_right (le_max_left _ _) (sq_nonneg h)
  have e1 : (n : ℝ) * h ≤ |kappa| * M * h ^ 2 := by
    calc (n : ℝ) * h = |kappa| * ((n : ℝ) / |kappa| * h) := by
          field_simp
      _ ≤ |kappa| * (M * h ^ 2) :=
          mul_le_mul_of_nonneg_left (le_trans hcurv' hCM) hk.le
      _ = |kappa| * M * h ^ 2 := by ring
  have e2 : h * (|kappa| * (M + 1)) ≤ (n : ℝ) := by
    have hmin : h ≤ (n : ℝ) / (|kappa| * (M + 1)) := by
      rw [hdef]
      exact min_le_right _ _
    exact (le_div_iff₀ hden).mp hmin
  have e3 : h * (|kappa| * (M + 1)) * (M * h) ≤ (n : ℝ) * (M * h) :=
    mul_le_mul_of_nonneg_right e2 (mul_nonneg hM0 hhpos.le)
  have e4 : (n : ℝ) * h * (M + 1) ≤ |kappa| * M * h ^ 2 * (M + 1) :=
    mul_le_mul_of_nonneg_right e1 (by linarith)
  have hnh : 0 < (n : ℝ) * h := mul_pos hn0 hhpos
  nlinarith [e3, e4, hnh]

/-- **THEOREM-tier constructor (T3, the headline).** Builds a
`RecognitionRatioBridge` from the constitutive deficit-source action data,
PROVING the `ratio_relation` field from J-stationarity.

Hypothesis audit (every hypothesis is structural; NONE is the ratio
relation or equivalent to it):
* `hn : 1 ≤ n` — at least one recognition channel (positivity side
  condition of `sourced_ratio_cubic_error`).
* `hh : 0 < h` — positive mesh scale (the structure's own
  `meshScale_pos` field).
* `hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ n * h` — source domination: the
  total source strength at each hinge is bounded by the mesh budget n*h.
  This bounds the INPUT data (coupling times deficit); it says nothing
  about xRatio, log xRatio, or the remainder, so it cannot smuggle the
  conclusion.

Fields produced BY DERIVATION:
* `xRatio σ := exp(n * arsinh(kappa σ * geomDeficit σ / n))` — DEFINED as
  the exponential of the total strain of the unique global minimizer of
  the sourced action `sourcedAction n (kappa σ * geomDeficit σ)`
  (`sourcedMinimizer`; uniqueness and global minimality are
  `sourced_unique_minimizer`, re-exported for this bridge as
  `ofStationarity_minimizer_grounding`).
* `remBound := n / 6` — the explicit constant inherited from the 1/6 of
  `sourced_ratio_cubic_error`.
* `ratio_relation` — PROVED, by `stationaryRatio_cubic`; not passed in.

MODEL disclosure: the sourced action's coupling term is the explicit
deficit-source constitutive choice of `HingeStationarityCore`. Every
bridge this constructor produces is derived from an explicit
deficit-source constitutive action plus J-stationarity, never from the
bare RecognitionLedger. -/
noncomputable def recognitionRatioBridge_ofStationarity {H : Type*}
    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) :
    RecognitionRatioBridge H where
  xRatio := fun σ =>
    Real.exp ((n : ℝ) * Real.arsinh (kappa σ * geomDeficit σ / n))
  xRatio_pos := fun _ => Real.exp_pos _
  kappa := kappa
  geometricDeficit := geomDeficit
  meshScale := h
  meshScale_pos := hh
  remBound := (n : ℝ) / 6
  remBound_nonneg := by positivity
  ratio_relation := fun σ =>
    stationaryRatio_cubic n hn (kappa σ * geomDeficit σ) h (hdom σ)

/-- **THEOREM (the derivation receipt).** The log of the constructed ratio
IS the total strain of the sourced minimizer with source
c = kappa σ * delta σ: this is the sense in which xRatio is defined FROM
the stationary point of the constitutive action, not posited. -/
theorem ofStationarity_log_xRatio_eq_minimizer_strain {H : Type*}
    (n : ℕ) (hn : 1 ≤ n) (kappa geomDeficit : H → ℝ) (h : ℝ) (hh : 0 < h)
    (hdom : ∀ σ, |kappa σ * geomDeficit σ| ≤ (n : ℝ) * h) (σ : H) :
    Real.log ((recognitionRatioBridge_ofStationarity n hn kappa geomDeficit
        h hh hdom).xRatio σ)
      = ∑ i, sourcedMinimizer n (kappa σ * geomDeficit σ) i := by
  rw [ofStationarity_log_xRatio n hn kappa geomDeficit h hh hdom σ]
  exact (stationaryLogRatio_total_strain n (kappa σ * geomDeficit σ)).symm