halfway_substrate
plain-language theorem explainer
Packages the midpoint map on strain space (average current strain with the least-cost carrier) as a cost-spending substrate for any hinge parameter a. Downstream non-uniqueness of the C2 motion residue cites this as one of two distinct models. Continuity is automatic; strict cost drop follows from the midpoint lying between the state and the minimum plus one-sided monotonicity of the sourced cost.
Claim. For every real $a$, the map $t \mapsto (t + \operatorname{arsinh} a)/2$ is a cost-spending substrate on the strain line: it is continuous, and at every strain $t \neq \operatorname{arsinh} a$ it strictly lowers the sourced recognition cost relative to $t$.
background
This module asks how far the recognition kernel reaches into gravity's C2 bridge. The kernel's cost content (reciprocity, normalization, the recognition composition law, unit log curvature, continuity on positive ratios) forces the cost functional $J$, but every clause is about the cost of a single ratio. None constrains maps on the strain ledger. Motion is therefore an extra adoption.
A cost-spending substrate is exactly that adoption, named as a structure: a continuous step map on the strain line that strictly lowers the sourced recognition cost at every state other than the least-cost carrier $\operatorname{arsinh} a$. It names no metric, rate, or gradient law. Sufficiency is already proved: every such substrate reaches the carrier under iteration from any initial strain.
The midpoint dynamics is the mildest geometric example of such a step: each iterate halves the distance in strain coordinate to the carrier. It sits beside the instantaneous collapse map as a second, inequivalent model of the same residue.
proof idea
Structure instance with step set to the midpoint map. Continuity is discharged by unfolding and fun_prop. For strict cost spending, fix $t \neq \operatorname{arsinh} a$ and split on the sign of $t - \operatorname{arsinh} a$. In each case the midpoint lies strictly between $t$ and the carrier (two linarith inequalities). On the left of the carrier the sourced cost is strictly antitone, on the right strictly monotone; applying the matching one-sided lemma yields a strict drop.
why it matters
The parent theorem is residue_has_two_models: the C2 residue has at least two distinct models, witnessed by the collapse substrate and this halfway substrate. That theorem is the module's punchline: the postulate does not name a dynamics. The kernel fixes $J$ (via the five cost premises and T5 J-uniqueness) but is silent on motion; the reciprocal involution already shows kernel cost content does not entail cost spending. Once cost spending is adopted as an explicit object, this definition shows even that residue is non-unique. It therefore marks the reach wall between forced cost structure and free strain dynamics in the Seven Gaps gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.