Gravity Seven Gaps Stationarity Bridge Closure Concrete Stationarity Bridge Nonv

/-- **THEOREM (T4 non-vacuity record).** The concrete instance has: the
prescribed signed deficits (+1/16 at hinge 0, -1/16 at hinge 1), a
STRICTLY NEGATIVE deficit at hinge 1 (the signed-deficit non-vacuity of
`ratioBridge_admits_negative_deficit`), mesh 1/8, unit coupling, and the
derived remainder constant remBound = 4/6 = 2/3 inherited from the cubic
error lemma. (Uses `decide` only for the Fin 2 literal disequality
1 ≠ 0, as in `RecognitionRatioBridge`.) -/
theorem concreteStationarityBridge_nonvacuous :
    concreteStationarityBridge.geometricDeficit 0 = 1 / 16 ∧
    concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) ∧
    concreteStationarityBridge.geometricDeficit 1 < 0 ∧
    concreteStationarityBridge.meshScale = 1 / 8 ∧
    concreteStationarityBridge.remBound = 2 / 3 ∧
    (∀ σ, concreteStationarityBridge.kappa σ = 1) := by
  have h0 : concreteStationarityBridge.geometricDeficit 0 = 1 / 16 := by
    show (if (0 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = 1 / 16
    rw [if_pos rfl]
  have h1 : concreteStationarityBridge.geometricDeficit 1 = -(1 / 16) := by
    show (if (1 : Fin 2) = 0 then (1 : ℝ) / 16 else -(1 / 16)) = -(1 / 16)
    have h10 : ¬((1 : Fin 2) = 0) := by decide
    rw [if_neg h10]
  refine ⟨h0, h1, ?_, rfl, ?_, fun _ => rfl⟩
  · rw [h1]
    norm_num
  · show ((4 : ℕ) : ℝ) / 6 = 2 / 3
    norm_num

/-- **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

/-- **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 (T2, uniform admissibility of the quadratic family).** For
kappa ≠ 0 the quadratic-deficit family is admissible on (0, h0) with the
UNIFORM constants C_K = n/|kappa| and C_R = n * h0^3 / 6: both constants
sit OUTSIDE the mesh scale, per the admissibility predicate, so the
derivation covers a genuine h -> 0 family, not a single point. Proof:
`sourced_ratio_isAdmissible` (reused, not re-derived) with the curvature
bound an exact equality |delta(h)| = (n/|kappa|) h^2, followed by the
constant simplification |kappa|^3 (n/|kappa|)^3 h0^3/(6 n^2)
= n h0^3/6. (As in `sourced_ratio_isAdmissible`: for h0 <= 0 the predicate
is vacuously true; the statement carries content exactly when 0 < h0.) -/
theorem quadraticSourceFamily_isAdmissible (n : ℕ) (hn : 1 ≤ n)
    (h₀ kappa : ℝ) (hκ : kappa ≠ 0) :
    (quadraticSourceFamily n kappa).IsAdmissible h₀ kappa
      ((n : ℝ) / |kappa|) ((n : ℝ) * h₀ ^ 3 / 6) := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  have hκ' : |kappa| ≠ 0 := abs_ne_zero.mpr hκ
  have hδ : ∀ h ∈ Set.Ioo (0 : ℝ) h₀,
      |(n : ℝ) / kappa * h ^ 2| ≤ (n : ℝ) / |kappa| * h ^ 2 := by
    intro h _
    rw [abs_mul, abs_div, abs_of_pos hn0, abs_of_nonneg (sq_nonneg h)]
  have hbase := sourced_ratio_isAdmissible n hn h₀ kappa
    ((n : ℝ) / |kappa|) (fun h => (n : ℝ) / kappa * h ^ 2) hδ
  have hconst : |kappa| ^ 3 * ((n : ℝ) / |kappa|) ^ 3 * h₀ ^ 3
      / (6 * (n : ℝ) ^ 2) = (n : ℝ) * h₀ ^ 3 / 6 := by
    field_simp
  rw [← hconst]
  exact hbase

/-- **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]