Gravity Seven Gaps Hinge Stationarity Core Sourced Cost Term Has Deriv At

The derivative of the sourced cost

In the framework's model of gravity, a small geometric mismatch at a hinge, called a deficit, carries a cost. The framework's library, a machine-checked collection of formal theorems, studies a specific cost function: the sum over cells of cosh(t_i) - 1, where t_i is a strain ratio. A theorem named sourced_costTerm_hasDerivAt proves that when this cost is minimized, the derivative of the optimal cost term with respect to the deficit parameter d is kappa * tanh(arsinh(kappa * d / n)), where kappa is a coupling constant and n is the number of cells.

This result corrects a prior suggestion. The earlier guess was kappa * sinh(arsinh(kappa * d / n)), which would be the chain-rule value if the cost term were simply a function of the minimized strain. The proved theorem shows the actual derivative is smaller, using tanh instead of sinh. The distinction matters because the derivative measures how sensitively the total cost responds to a change in the deficit, a quantity that feeds into the framework's account of gravitational dynamics.

The theorem is part of a larger, honest accounting of what follows from the framework's core cost function J(x) = (x + 1/x)/2 - 1. The library also proves that a naive approach, imposing a budget and then concluding a ratio, is circular, and that a raw Stokes route cannot source a nonzero hinge deficit. The derivative theorem itself is a clean, kernel-checked statement about a specific function, not a claim about the physical interpretation of that function.

What the theorem does not claim is equally important. It does not assert that the cost function it differentiates is the unique or correct description of gravity. The cost function is a constitutive MODEL, a definitional choice, not a derived consequence of the bare recognition ledger. The theorem only establishes a property of that chosen model. It also does not claim that the derivative value has a direct physical meaning, such as being a force or an observable; it is a mathematical fact about the model's response to a parameter.

/-- **THEOREM (chain-rule derivative of the optimal cost term).** The
derivative of delta ↦ n*(cosh(arsinh(kappa*delta/n)) - 1) is
kappa * tanh(arsinh(kappa*delta/n)) = kappa*(kappa*delta/n)/sqrt(1+(kappa*delta/n)^2).
This CORRECTS the spec's suggested value kappa*sinh(arsinh(.)): the
arsinh chain factor 1/sqrt(1+y^2) turns sinh into tanh. -/
theorem sourced_costTerm_hasDerivAt (n : ℕ) (hn : 1 ≤ n) (kappa d : ℝ) :
    HasDerivAt
      (fun z => (n : ℝ) * (Real.cosh (Real.arsinh (kappa * z / n)) - 1))
      (kappa * Real.tanh (Real.arsinh (kappa * d / n))) d := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  have hs_pos : 0 < Real.sqrt (1 + (kappa * d / n) ^ 2) :=
    Real.sqrt_pos.mpr (by positivity)
  have hinner : HasDerivAt (fun z : ℝ => kappa * z / (n : ℝ))
      (kappa / n) d := by
    have h := ((hasDerivAt_id d).const_mul kappa).div_const (n : ℝ)
    simpa using h
  have harsinh := hinner.arsinh
  have hcosh := harsinh.cosh
  have htotal := (hcosh.sub_const 1).const_mul (n : ℝ)
  convert htotal using 1
  rw [Real.tanh_arsinh, smul_eq_mul, Real.sinh_arsinh]
  field_simp

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

/-- 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 cost function is the unique or physically correct model of gravity. The theorem does not claim the derivative value is a physical observable such as a force. The theorem does not claim the cost function is derived from the bare recognition ledger without a constitutive choice.

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: