collapseStep
plain-language theorem explainer
Constant strain map sending every state straight to the least-cost point arsinh(a). It is one explicit model of cost-spending dynamics on the strain line. Cited when showing the C2 residue postulate admits at least two distinct continuous cost-lowering steps. Definition is a one-line constant function.
Claim. For each real parameter $a$, define the collapse step as the constant map on the strain line $t \mapsto \operatorname{arsinh}(a)$. Every strain is sent in one step to the least-cost state.
background
This module asks how far the recognition kernel reaches. The kernel's cost content is the premise package that forces the cost on positive ratios to be $J$ (reciprocal, normalized, RCL, unit log curvature, continuous). Those premises quantify only over single ratios; none constrains a map on the strain ledger.
The C2 bridge therefore needs an extra residue: continuous strain dynamics that strictly lowers recognition cost at every state other than the least-cost state (CostSpendingSubstrate). The reciprocal involution $t \mapsto -t$ already shows the kernel alone does not force that residue: it preserves bare $J$-cost and never reaches the carrier.
collapseStep is the extreme cost-spending model: jump every strain immediately to the least-cost coordinate.
proof idea
One-line definition. The body is the constant function fun _ => Real.arsinh a, independent of the input strain. Continuity is immediate (continuous_const); cost-spending is discharged downstream by comparing source cost away from the least-cost state.
why it matters
Feeds collapse_substrate, which packages this step as a CostSpendingSubstrate. That substrate is one of the two witnesses in residue_has_two_models: the residue has at least two distinct models (collapse versus halfway). The module's structural claim is that the kernel fixes cost, not motion; this map is the sharpest cost-spending extreme used to make that non-uniqueness concrete for the C2 bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.