Gravity Seven Gaps Hinge Stationarity Core Sourced Value Eq Action Min

The sourced value identity

The declaration sourcedValue_eq_action_min proves a precise identity about a model of gravity. The model works with a discrete record of events, called a ledger, where each cell in a mesh carries a strain ratio. The framework defines an action, a total cost over all cells, as the sum of a recognition cost plus a coupling term that sources the strain from a deficit. The theorem states that the value of this action at its unique minimum equals a simple closed-form expression: n * (cosh(arsinh(kappa * d / n)) - 1) - kappa * d * arsinh(kappa * d / n), where n is the cell count, kappa a coupling constant, and d the deficit.

This identity is the hinge of a larger argument. It shows that minimizing the sourced action produces a strain distribution where every cell carries the same ratio, and the total logarithmic strain equals the deficit up to a cubic error term. The proof is machine-checked, meaning a computer verified every step from the axioms. The error term has an explicit constant of 1/6, so the approximation is not vague but bounded: |n * arsinh(c/n) - c| ≤ |c|^3 / (6 n^2). This gives a quantitative handle on how quickly the model approaches the naive budget relation as the mesh refines.

What the theorem does not claim is just as important. The coupling term, the part that injects the deficit into the action, is a constitutive choice, a model input, not something forced by the framework's core principles. The framework's recognition cost, the function J(x) = (x + 1/x)/2 - 1, appears in the action through a separate kernel equation, but the sourced coupling is added by hand. The theorem proves the mathematics of that chosen model, not that the model is the only possible one or that it follows from the bare ledger.

In plain terms, the declaration is a clean statement about a specific construction: given this action, the minimum has this value, and the minimizer splits evenly. It is a theorem about the model, not a theorem that the model is true of the physical world. The physical bridge, connecting this discrete ledger to continuous spacetime geometry, remains open. What the theorem secures is the internal consistency of the sourced stationary ratio approach: the minimization works, the error is controlled, and the value function has a clean derivative, all verified by machine.

/-- **THEOREM.** The optimal value function IS the sourced action
evaluated at its unique minimizer (with source c = kappa*d). -/
theorem sourcedValue_eq_action_min (n : ℕ) (hn : 1 ≤ n) (kappa d : ℝ) :
    sourcedValue n kappa d
      = sourcedAction n (kappa * d) (sourcedMinimizer n (kappa * d)) := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  unfold sourcedValue sourcedAction sourcedMinimizer
  rw [Finset.sum_const, Finset.sum_const, Finset.card_univ,
    Fintype.card_fin, nsmul_eq_mul, nsmul_eq_mul]
  field_simp

/-- **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 (item 3, sourced unique minimizer).** For every n (no
n >= 1 hypothesis is needed; at n = 0 both conjuncts are trivially true
on the empty tick set) and every total source strength c, the sourced
action
Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i over t : Fin n → ℝ has
the unique global minimizer t_i = arsinh(c/n) for all i. The stationarity
condition sinh t_i = c/n is genuinely FORCED here (contrast with the
circular raw 1b route, `budget_implies_ratio_without_stationarity`), but
only because the deficit-source coupling was supplied as a MODEL input. -/
theorem sourced_unique_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
    sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c t ∧
      (sourcedAction n c t = sourcedAction n c (sourcedMinimizer n c) →
        t = sourcedMinimizer n c) :=
  ⟨sourced_minimizer_le n c t, sourced_minimizer_unique n c t⟩

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

What this page does not claim

The theorem does not claim the sourced action model is derived from the bare recognition ledger. It does not claim the model describes actual gravity in the physical world. It does not claim the coupling constant kappa has a specific numerical value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: