costSpendingSubstrate_nonempty
plain-language theorem explainer
For every real source parameter, the cost-spending-substrate postulate is inhabited: the banked one-dimensional strain step is continuous and strictly lowers sourced recognition cost off the least-cost carrier. C2-bridge and gravity authors cite this as consistency of the motion residue the kernel does not force. The proof is a direct witness construction from the strain step, its continuity, and one-dimensional descent.
Claim. For every real $a$, the type of cost-spending substrates at $a$ is nonempty: there exists a continuous map $s:\mathbb{R}\to\mathbb{R}$ such that whenever $t\neq\operatorname{arsinh} a$, the sourced recognition cost of $s(t)$ is strictly smaller than that of $t$.
background
This module asks how far the recognition kernel reaches into strain dynamics. The kernel's cost content is exactly the premise package that forces the unique cost $J$ (reciprocity, normalization, the recognition composition law, unit log curvature, continuity on positive ratios). Those premises quantify only over single ratios; they say nothing about maps on the strain ledger or about motion.
A cost-spending substrate at source parameter $a$ is the named C2-bridge residue: a continuous step on the hinge channel's strain line that strictly lowers sourced recognition cost at every state other than the least-cost carrier $t=\operatorname{arsinh} a$. It names no metric, rate, or gradient law, only continuity and strict cost decrease off the carrier.
The reciprocal involution $t\mapsto -t$ (ledger reciprocity $x\mapsto 1/x$) is continuous, preserves bare $J$-cost, and never reaches the carrier from nonzero strain. So the kernel alone does not entail cost-spending. The present theorem answers the consistency question for the explicit postulate that remains.
proof idea
Term-mode witness construction. Package the banked strain step strainStep1 a as the substrate map, discharge continuity by strainStep1_continuous a, and prove the spends-cost clause by applying the one-dimensional descent inequality descent_one_dim_lt a t. The residual fixed-point case is reduced via step_fixed_iff_arsinh: if the residual vanishes then the unfolded strain step equals $t$, so $t$ is the arsinh carrier, contradicting the off-carrier hypothesis. Algebra closes with a short ring normalization after rewriting the residual.
why it matters
Closes the consistency half of the module's reach-wall argument. The kernel fixes configuration cost (T5 $J$-uniqueness via the recognition composition law) but not motion; the reciprocal involution is the structural counterexample. What the C2 bridge still adopts is therefore an explicit object, and this theorem shows that object is inhabited rather than contradictory: the banked gradient step is a concrete cost-spending substrate.
Downstream, every cost-spending substrate reaches the sourced least-cost carrier under iteration (CostSpendingSubstrate.reaches_carrier). No external used-by edges are recorded yet; the local consumer is that sufficiency theorem and the surrounding SevenGaps gravity stack. Framework landmarks in view: $J$-cost uniqueness, the strain coordinate on the ratio ledger, and the separation between cost law and dynamics that the forcing chain never fills.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.