Gravity Seven Gaps Stationarity Bridge Closure Of Stationarity Log X Ratio Eq Mi

/-- **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.** The total strain of the unique sourced minimizer
(`sourcedMinimizer`, t_i = arsinh(c/n)) is n * arsinh(c/n): the quantity
whose exponential the constructor uses as xRatio. This is the kernel link
between "xRatio is defined from the minimizer" and the closed-form
expression the cubic bound is stated about. -/
theorem stationaryLogRatio_total_strain (n : ℕ) (c : ℝ) :
    ∑ i, sourcedMinimizer n c i = (n : ℝ) * Real.arsinh (c / n) := by
  simp only [sourcedMinimizer]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]

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