CostSpendingSubstrate
plain-language theorem explainer
A cost-spending substrate is a continuous map on hinge-channel strain space that strictly lowers sourced recognition cost at every state other than the least-cost carrier. C2-bridge and strain-dynamics work cite it as the weakest motion postulate the bridge needs: no metric, step law, rate, or gradient. As a structure it only packages the step map, continuity, and the strict cost-decrease field.
Claim. For a real hinge parameter $a$, a cost-spending substrate is a continuous map $\mathrm{step}:\mathbb{R}\to\mathbb{R}$ on strain space such that whenever $t\neq\operatorname{arsinh} a$, the sourced recognition cost of $\mathrm{step}(t)$ is strictly smaller than that of $t$.
background
The module asks how far the recognition kernel reaches. Kernel cost content is exactly the premise package that forces the cost to be $J$: reciprocity, normalization, the recognition composition law, unit log curvature, and continuity on positive ratios. Every premise is about the cost of a single ratio; none quantifies over a map on the ledger or a sequence of postings. The kernel fixes what a configuration costs, not how it moves.
The C2 bridge's stationarity premise reduces to a residue: continuous strain dynamics that strictly lowers recognition cost away from the least-cost state (the carrier at $\operatorname{arsinh} a$). That residue is named here as an explicit object. The ledger's own reciprocal involution $t\mapsto -t$ is continuous, preserves bare cost, and never reaches the carrier from nonzero strain, so the kernel alone does not force cost-spending motion.
proof idea
Structure definition, not a proved theorem. Three fields: a real map on strain, a Continuous certificate, and a pointwise strict inequality for sourced cost off the carrier. No tactic or term proof beyond the field types.
why it matters
Names the whole of what the C2 bridge assumes about motion, so the adoption is explicit rather than smuggled. Downstream, the banked gradient step inhabits the type (costSpendingSubstrate_nonempty), proving consistency. Collapse and halfway steps give two distinct models (residue_has_two_models), which yields that no single flow is fixed by the residue (no_unique_dynamics_from_residue). Sufficiency is separate: every such substrate's iterates tend to the carrier. The structure is the reach-wall hinge between kernel-fixed $J$-cost and unforced dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.