Gravity Seven Gaps Hinge Stationarity Core Sourced Ratio Cubic Error

/-- **THEOREM (item 4, cubic error of the sourced ratio, constant 1/6).**
|n * arsinh(c/n) - c| <= |c|^3 / (6 n^2) for n >= 1. This is the honest
form of the bridge expansion: the sourced stationary log ratio
n * arsinh(c/n) equals the deficit source c = kappa*delta up to an
explicitly bounded cubic error. -/
theorem sourced_ratio_cubic_error (n : ℕ) (hn : 1 ≤ n) (c : ℝ) :
    |(n : ℝ) * Real.arsinh (c / n) - c|
      ≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  have hkey : (n : ℝ) * Real.arsinh (c / n) - c
      = (n : ℝ) * (Real.arsinh (c / n) - c / n) := by
    field_simp
  rw [hkey, abs_mul, abs_of_pos hn0]
  have hcn : |c / (n : ℝ)| ^ 3 = |c| ^ 3 / (n : ℝ) ^ 3 := by
    rw [abs_div, abs_of_pos hn0, div_pow]
  calc (n : ℝ) * |Real.arsinh (c / n) - c / n|
      ≤ (n : ℝ) * (|c / (n : ℝ)| ^ 3 / 6) :=
        mul_le_mul_of_nonneg_left (abs_arsinh_sub_self_le (c / n)) hn0.le
    _ = |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
        rw [hcn]
        field_simp

/-- **THEOREM (cubic error of arsinh, constant 1/6).**
|arsinh y - y| <= |y|^3 / 6 for ALL y (nonnegative branch from the two
bounds above, negative branch by oddness of arsinh). -/
theorem abs_arsinh_sub_self_le (y : ℝ) :
    |Real.arsinh y - y| ≤ |y| ^ 3 / 6 := by
  rcases le_or_gt 0 y with hy | hy
  · have h1 := arsinh_le_self_of_nonneg hy
    have h2 := self_sub_cube_le_arsinh hy
    rw [abs_of_nonneg hy,
      abs_of_nonpos (by linarith : Real.arsinh y - y ≤ 0)]
    linarith
  · have hy' : 0 ≤ -y := by linarith
    have h1 := arsinh_le_self_of_nonneg hy'
    have h2 := self_sub_cube_le_arsinh hy'
    rw [Real.arsinh_neg] at h1 h2
    have hcube : (-y) ^ 3 = -(y ^ 3) := by ring
    rw [hcube] at h2
    rw [abs_of_neg hy,
      abs_of_nonneg (by linarith : 0 ≤ Real.arsinh y - y)]
    have hgoal : (-y) ^ 3 = -(y ^ 3) := by ring
    rw [hgoal]
    linarith

/-- **THEOREM (kill record C6, the raw Stokes route).** For a coboundary
strain s i j = f i - f j and any cyclic chain of cells v 0, v 1, ..., v m
with v m = v 0, the sum of strains around the cycle telescopes to zero.
Exact/coboundary substrate strains can NEVER sum to a nonzero deficit
around a closed hinge link: the raw Stokes route to the bridge relation is
dead, kernel-checked. -/
theorem closedCycle_coboundary_sum_eq_zero {Λ : Type*} {s : Λ → Λ → ℝ}
    (hs : IsCoboundary s) (v : ℕ → Λ) (m : ℕ) (hcycle : v m = v 0) :
    ∑ k ∈ Finset.range m, s (v k) (v (k + 1)) = 0 := by
  obtain ⟨f, hf⟩ := hs
  calc ∑ k ∈ Finset.range m, s (v k) (v (k + 1))
      = ∑ k ∈ Finset.range m,
          ((fun j => f (v j)) k - (fun j => f (v j)) (k + 1)) :=
        Finset.sum_congr rfl fun k _ => hf (v k) (v (k + 1))
    _ = f (v 0) - f (v m) := Finset.sum_range_sub' (fun j => f (v j)) m
    _ = 0 := by rw [hcycle]; ring

/-- **THEOREM (kill record raw 1b, the budget circularity).** If the
holonomy budget sum_i t_i = kappa*delta is IMPOSED, then the "conclusion"
log ratio = kappa*delta holds with NO optimization used: the proof term is
the budget hypothesis itself. This records, kernel-checked, that the naive
1b formulation (impose budget, minimize, conclude ratio) is CIRCULAR: the
budget already contains the conclusion; stationarity added nothing. -/
theorem budget_implies_ratio_without_stationarity {n : ℕ} (t : Fin n → ℝ)
    (kappa delta : ℝ) (hbudget : ∑ i, t i = kappa * delta) :
    naiveLogRatio n t = kappa * delta := hbudget

/-- The sourced action Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i:
the J-cost of the per-tick strains (via J(exp t) = cosh t - 1,
`Cost.Jcost_exp_cosh`) plus an explicit deficit-source coupling of total
strength c = kappa*delta, split evenly across the n ticks. The coupling
term is the MODEL input; see the module header. -/
noncomputable def sourcedAction (n : ℕ) (c : ℝ) (t : Fin n → ℝ) : ℝ :=
  (∑ i, (Real.cosh (t i) - 1)) - c / n * ∑ i, t i