Gravity Seven Gaps Stationarity Bridge Closure Quadratic Source Family Deficit N

/-- **THEOREM (nontriviality of the family: nonzero deficit).** For
kappa ≠ 0 and every nonzero mesh h, the quadratic family's deficit is
nonzero: the admissibility above is about a genuinely sourced family, not
the trivial delta = 0 one. -/
theorem quadraticSourceFamily_deficit_ne_zero (n : ℕ) (hn : 1 ≤ n)
    (kappa h : ℝ) (hκ : kappa ≠ 0) (hh : h ≠ 0) :
    (quadraticSourceFamily n kappa).deficit h ≠ 0 := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  show (n : ℝ) / kappa * h ^ 2 ≠ 0
  exact mul_ne_zero (div_ne_zero (ne_of_gt hn0) hκ) (pow_ne_zero 2 hh)

/-- **THEOREM (nontriviality of the family: nonzero log ratio).** For
kappa ≠ 0 and every nonzero mesh h, the family's stationary log ratio
log x(h) = n * arsinh(h^2) is strictly positive: the bridge relation the
admissibility certifies is a relation between genuinely nonzero
quantities. -/
theorem quadraticSourceFamily_logRatio_pos (n : ℕ) (hn : 1 ≤ n)
    (kappa h : ℝ) (hκ : kappa ≠ 0) (hh : h ≠ 0) :
    0 < Real.log ((quadraticSourceFamily n kappa).ratio h) := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  show 0 < Real.log (Real.exp
    ((n : ℝ) * Real.arsinh (kappa * ((n : ℝ) / kappa * h ^ 2) / n)))
  rw [Real.log_exp]
  have harg : kappa * ((n : ℝ) / kappa * h ^ 2) / n = h ^ 2 := by
    field_simp
  rw [harg]
  have hh2 : 0 < h ^ 2 :=
    lt_of_le_of_ne (sq_nonneg h) (Ne.symm (pow_ne_zero 2 hh))
  exact mul_pos hn0 (Real.arsinh_pos_iff.mpr hh2)

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