module module high

`IndisputableMonolith.Gravity.SevenGaps.StrainDescent`

Defines the sourced strain cost and the discrete gradient descent step that drives a hinge link's strain toward the least-cost carrier. Gravity and ledger workers cite it when reducing C2 stationarity to a dynamical principle. The module builds the residual, envelope, and step-size bounds from hyperbolic identities and elementary integral comparisons.

claimPer-channel sourced cost $\psi_a(s)=\cosh s-1-a\cdot s$. Strain residual, envelope, and step size control a discrete descent map $s\mapsto s-\eta\,\psi_a'(s)$ on hinge strain space, with positivity and contraction bounds that force convergence to the sourced stationary ratio.

background

In the Seven Gaps gravity stack, each hinge link carries a real strain coordinate $s$. The unsourced J-cost is $\cosh s-1$ (the T5 unique cost on the positive reals). A linear source term $-a\cdot s$ tilts the landscape; the resulting per-channel cost is $\psi_a(s)=\cosh s-1-a\cdot s$.

The upstream hinge-stationarity core already identifies the unique critical point of $\psi_a$ as the sourced stationary ratio. This module equips that landscape with a residual (how far the current strain sits from stationarity), a positive envelope that majorizes the residual, and a step size small enough that a single gradient step strictly decreases the envelope.

Local setting: pure real analysis on $\mathbb{R}$ with Mathlib hyperbolic and integral lemmas; no RS-internal axioms. The import surface is Mathlib plus the hinge-stationarity core (and, transitively, the ledger-energy bridge).

proof idea

Definitions introduce $\psi_a$, the residual, the envelope, and the admissible step size. Positivity lemmas show the envelope is at least one and strictly positive, and that the step size lies in $(0,1]$.

Comparison lemmas reduce envelope decrease to elementary facts: $\cosh$ is increasing on $[0,\infty)$, and the integrals of $\sinh$ and $\cosh$ supply explicit antiderivatives for the residual and its derivative. The one-step map is then shown to cut the envelope, which is the discrete Lyapunov step used downstream.

why it matters in Recognition Science

Feeds DescentPrincipleUniversality, which states that the metric is a choice that cannot matter once the carrier dynamics is fixed. Downstream doc-comment: the carrier dynamics is a theorem; the gradient step on a hinge link's strain space converges to the sourced least-cost carrier (StrainDescent). That reduces the C2 stationarity premise to one dynamical principle: the substrate's strain state follows steepest descent on $\psi_a$.

In the broader RS gravity program this closes the dynamical half of the seven-gaps hinge argument: stationarity is not postulated, it is the attractor of a proved descent map built from the unique J-cost (T5) with a linear source. No open scaffolding remains inside the module; every named sibling is a definition or a proved bound.

scope and limits

Does not prove global multi-link or continuum spacetime convergence.
Does not choose a physical value of the source parameter $a$.
Does not derive Einstein equations or Newtonian limits.
Does not address discrete ledger tick timing or eight-tick octave structure.
Does not claim uniqueness of the discrete step rule beyond envelope decrease.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore module_import

declarations in this module (36)

def sourceCost1 L83
def strainResidual L86
def strainEnvelope L91
def strainStepSize L97
def strainStep1 L100
theorem strainEnvelope_ge_one L103
theorem strainEnvelope_pos L108
theorem strainStepSize_pos L112
theorem strainStepSize_le_one L117
theorem cosh_le_cosh_of_nonneg_of_le L124
theorem integral_sinh L142
theorem integral_cosh L150
theorem sinh_le_mul_cosh L159
theorem integral_id_half_sq L173
theorem integral_sq_half_third L185
theorem cosh_sub_one_le_sq_half_cosh L197
theorem abs_sinh_sub_self_le_sixth L229
theorem step_one_dim_sub L309
theorem cosh_step_le_cosh_abs_residual L320
theorem correction_le_half L336
theorem descent_one_dim L435
theorem descent_one_dim_lt L443
theorem step_fixed_iff_arsinh L458
theorem abs_sinh_eq_sinh_abs L480
theorem contraction_one_dim L493
def strainOrbit L604
theorem strainOrbit_abs_le L609
theorem strainOrbit_tendsto L726
def strainStepVec L741
theorem sourcedAction_eq_sum_sourceCost1 L745
theorem sourcedAction_step_le L751
theorem sourcedAction_step_lt L767
theorem stepVec_fixed_iff_minimizer L788
def strainStepVecOrbit L801
theorem strainStepVecOrbit_apply L807
theorem strainStepVec_tendsto_minimizer L818