collapse_substrate
plain-language theorem explainer
Constructs the constant collapse dynamics on a hinge channel: every strain is sent in one step to the least-cost carrier arsinh(a). It is the simplest model of a cost-spending substrate (continuous, strictly cost-lowering off the carrier). Downstream work cites it as one of two inequivalent models showing the C2 motion residue is not unique.
Claim. For each real source parameter $a$, the constant map $t \mapsto \operatorname{arsinh} a$ is a cost-spending substrate: it is continuous, and for every strain $t \neq \operatorname{arsinh} a$ the sourced recognition cost strictly decreases under the map.
background
This module asks how far the recognition kernel reaches into strain dynamics. The kernel fixes the cost functional $J$ (reciprocal, normalized, RCL, unit log curvature, continuous on positive ratios) but says nothing about motion on the ratio ledger. The C2 bridge therefore adopts an extra residue: a continuous step that strictly lowers sourced recognition cost off the least-cost state.
That residue is packaged as CostSpendingSubstrate: a continuous map step : ℝ → ℝ on the hinge strain coordinate such that sourceCost1 a (step t) < sourceCost1 a t whenever $t \neq \operatorname{arsinh} a$. Sufficiency is already proved: every such substrate reaches the carrier under iteration.
The constant collapse map sends every strain straight to $\operatorname{arsinh} a$. The key upstream fact is that $\operatorname{arsinh} a$ is the strict global minimum of the sourced cost, so any off-carrier point has strictly higher cost than the image.
proof idea
Structure instance for the cost-spending substrate. The step field is the constant collapse map. Continuity is continuous_const. The cost-spending obligation reduces, for $t \neq \operatorname{arsinh} a$, to the strict global-minimum theorem for the sourced cost at the carrier, applied once.
why it matters
Names the simplest concrete model of the C2 motion residue: instantaneous collapse to the least-cost carrier. The parent theorem residue_has_two_models pairs this model with the halfway (distance-halving) substrate to prove the residue has at least two distinct dynamics, so the postulate does not name a unique law of motion.
That non-uniqueness is the module's structural point: the kernel forces cost, not dynamics. The reciprocal involution already shows kernel cost content does not entail cost-spending; this definition supplies a positive model inside the residue class used by the gravity bridge. It does not touch T5–T8 forcing, RCL uniqueness of $J$, or the mass ladder; it only populates the motion side of the SevenGaps C2 package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.