halfwayStep
plain-language theorem explainer
Defines the affine map that sends strain coordinate t halfway toward the least-cost point arsinh(a). Gravity and C2-bridge work cite it as one concrete cost-spending step on the strain line. The body is a one-line function definition, not a proof.
Claim. For fixed $a \in \mathbb{R}$, the halfway step is the map $t \mapsto \frac{t + \operatorname{arsinh} a}{2}$ on the real strain line. It moves every strain halfway toward the least-cost state $\operatorname{arsinh} a$.
background
This module asks how far the recognition kernel reaches once cost is fixed. Kernel cost content is the five-premise package that forces the cost functional to be $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 ledger or sequences of postings.
The C2 bridge therefore needs an extra residue: continuous strain dynamics that strictly lowers recognition cost away from the least-cost state (DescentPrincipleUniversality, packaged here as CostSpendingSubstrate). The module shows that residue is not forced by the kernel. The reciprocal involution $t \mapsto -t$ preserves $J$ exactly and never reaches the carrier, so kernel cost content alone does not entail cost spending.
In the strain coordinate the least-cost point for parameter $a$ is $\operatorname{arsinh} a$. The halfway map is one elementary continuous step that moves every $t$ toward that point by half the remaining distance.
proof idea
Pure definition: no tactics, no lemmas. The map is written as the affine function $(t + \operatorname{arsinh} a)/2$. Continuity and the cost-spending inequality are proved later when the map is packaged into halfway_substrate.
why it matters
Supplies one of the two concrete step maps that witness non-uniqueness of the C2 residue. Downstream, halfway_substrate wraps it as a CostSpendingSubstrate, and residue_has_two_models compares it to collapseStep to prove there exist at least two distinct cost-spending dynamics for every $a$. That theorem is the module's main punchline: the named postulate does not name a dynamics.
In the broader Recognition picture this sits on the gravity/C2 side of the forcing chain. The kernel (T5 $J$-uniqueness via RCL and the related cost axioms) fixes configuration cost; motion toward the least-cost state is an independent modeling choice. The halfway map is the mild, contractive choice, complementary to instantaneous collapse, and makes the multiplicity claim fully constructive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.