reciprocalInvolution_continuous
plain-language theorem explainer
The reciprocal involution on strain space, the map t ↦ −t (log-coordinate form of ratio reciprocity x ↦ 1/x), is continuous as a real map. Anyone building the kernel-reach counterexample cites this to discharge the continuity hypothesis on that dynamics. The proof is a one-line appeal to continuity of negation on ℝ.
Claim. The reciprocal involution on the strain line, $S(t) = -t$ (equivalently ratio reciprocity $x \mapsto 1/x$ in logarithmic strain coordinates), is a continuous map $\mathbb{R} \to \mathbb{R}$.
background
This module asks how far the recognition kernel reaches: it fixes what a configuration costs, not how configurations move. 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 calibration, and continuity on positive ratios). None of those premises quantifies over a dynamics on the ratio ledger.
The structural counterexample is the ledger's own reciprocal involution. On ratios it is $x \mapsto 1/x$; in the strain coordinate $t = \mathrm{arsinh}$-style log chart it is simply $t \mapsto -t$. Reciprocity of $J$ is exactly invariance of bare cost under this map. Upstream, reciprocal maps appear throughout the algebra and ledger layers (the reciprocal automorphism on positive ratios, reciprocal recognition events with inverted ratio), all encoding the same $x \leftrightarrow 1/x$ symmetry that the recognition composition law builds in.
Continuity of that involution is the first elementary fact needed before one can exhibit it as a continuous strain dynamics that preserves cost and never descends to the carrier.
proof idea
One-line term proof: the involution is definitionally negation on $\mathbb{R}$, so Mathlib's continuous_neg applies directly. No local lemmas are needed beyond the definition of the involution as $t \mapsto -t$.
why it matters
This is a small continuity lemma inside the Seven Gaps gravity stack, but it is load-bearing for the reach wall. Downstream, kernel_cost_content_does_not_entail_cost_spending packages kernel cost content for $J$ together with an existential continuous strain map that preserves source cost everywhere and fails strict cost decrease off the least-cost state; the witness is exactly this involution, and continuity is discharged here. The sharper logical form no_kernel_derivation_of_residue then shows the implication "kernel cost premises $\Rightarrow$ every continuous strain map spends cost off the carrier" is false.
In framework terms, the result separates T5-style $J$-uniqueness (what configurations cost) from any descent or cost-spending postulate on motion. The C2 bridge's stationarity residue is therefore an explicit named substrate assumption, not a kernel theorem. Without continuity of the involution, the counterexample would not sit inside the continuous-dynamics class the residue quantifies over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.