module module moderate

`IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality`

Universality of the strain descent principle: continuous dynamics that strictly lower recognition cost everywhere except the least-cost carrier. The module packages derivative, coercivity, and monotonicity facts for the sourced cost, plus the descent field whose zeros are exactly the stationary states. Gravity and C2-bridge work cites it to shrink stationarity to a weak dynamical residue. Argument is calculus on the one-dimensional cost plus elementary hyperbolic inequalities.

claimFor the sourced recognition cost $C_1$ on the link, $C_1'(x)$ equals the residual (recognition phase minus source). $C_1$ is continuous and coercive; it is strictly monotone on each side of its unique minimizer; and $C_1(x)$ is strictly above the minimum whenever $x$ is not that minimizer. The descent field vanishes if and only if the state is least-cost.

background

The C2 bridge needs an existence half of stationarity adoption: the substrate attains the sourced least-cost carrier on each hinge link. Upstream StrainDescent supplies a convergent least-cost flow on the link and ties it to the canonical tick update from the recognition-update descent wall.

This module isolates the analytic core of that flow. The sourced cost $C_1$ is the recognition cost with an external source term. Its derivative is identified with the residual (recognition phase minus source), so gradient descent on $C_1$ is residual-driven. Hyperbolic comparison lemmas (self versus $\sinh$, quadratic bounds versus $\cosh$) control growth and give coercivity and one-sided strict monotonicity.

The local setting is the SevenGaps gravity stack: reduce physical stationarity premises to checkable dynamical inequalities on strain, without fixing a full equation of motion.

proof idea

Not a single theorem: a short calculus package. Derivative and continuity of $C_1$ are recorded first (hasDerivAt, explicit derivative, continuity). Coercivity and strict mono/anti facts on the two rays about the minimizer use the hyperbolic comparison lemmas. From those follow strict inequality off the minimizer and a minimum bound. The descent field is then defined so that its zeros match least-cost states (descentField_zero_iff). Overall shape: identify residual with $C_1'$, then read strict descent and uniqueness of the stationary point from one-dimensional real analysis.

why it matters in Recognition Science

Downstream StrainDynamicsKernelReach takes this as the weakest sufficient form of the C2 stationarity premise: strain dynamics continuous and strictly cost-lowering off the least-cost state. That parent module then asks how far the recognition kernel reaches (it fixes the cost, not the motion). Closing universality here lets the gravity stack separate cost geometry from trajectory law, which is the residue left after the forcing-chain and eight-tick structure have fixed the discrete recognition skeleton. Without these lemmas, stationarity adoption would still need a stronger, less checkable existence postulate on each link.

scope and limits

Does not derive a full equation of motion for strain, only cost-lowering dynamics.
Does not prove global existence of flows in higher dimensions or on networks of hinges.
Does not fix numerical values of $G$, masses, or galactic rotation curves.
Does not discharge the full C2 bridge; only the descent-universality residue used downstream.
Does not address quantum or relativistic corrections beyond the classical cost on the link.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.StrainDynamicsKernelReach module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.StrainDescent module_import

declarations in this module (25)

theorem sourceCost1_hasDerivAt L99
theorem deriv_sourceCost1 L108
theorem sourceCost1_continuous L112
theorem self_le_sinh L117
theorem one_add_sq_div_two_le_cosh L132
theorem sourceCost1_coercive L153
theorem sourceCost1_strictMonoOn L170
theorem sourceCost1_strictAntiOn L183
theorem sourceCost1_lt_of_ne L196
theorem sourceCost1_min_le L202
def descentField L213
theorem descentField_zero_iff L218
theorem descentField_descends L240
theorem metric_not_forced L256
theorem cost_decreasing_dynamics_converges L285
theorem rest_state_forced L372
theorem cost_decreasing_dynamics_converges' L401
theorem continuity_is_load_bearing L413
theorem strainResidual_continuous L456
theorem strainEnvelope_continuous L460
theorem strainStepSize_continuous L465
theorem strainStep1_continuous L470
theorem strainStep1_converges_by_universality L478
theorem descent_principle_residue L499
theorem link_channels_converge L515