reciprocalInvolution
plain-language theorem explainer
The reciprocal involution on the strain line is ordinary negation $t\mapsto -t$, the strain form of the ledger map $x\mapsto 1/x$. Kernel-reach and gravity arguments cite it as the canonical continuous motion that preserves bare recognition cost while never descending to the carrier. It is introduced by a one-line definitional assignment.
Claim. Define the reciprocal involution on the real strain line by $t \mapsto -t$. Under the strain coordinate $t = \log x$, this is the image of the ledger reciprocity map $x \mapsto 1/x$.
background
This module asks how far the recognition kernel reaches into dynamics. The kernel's 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). Every premise is a statement about the cost of a single ratio; none quantifies over a map on the ledger or a sequence of postings. The kernel therefore fixes what a configuration costs, not how it moves.
Strain is the logarithmic coordinate $t$ on the ratio ledger. In that coordinate the ledger's own reciprocity $x\mapsto 1/x$ becomes ordinary sign flip $t\mapsto -t$. The module uses this map as the structural counterexample to the claim that kernel cost content already forces cost-spending dynamics (the C2 residue / descent principle).
proof idea
One-line definition: the map is identified with real negation. No lemmas are applied; downstream continuity, cost preservation, and orbit statements unpack this assignment directly (e.g. via continuous_neg and Real.cosh_neg).
why it matters
This is the named counterexample that builds the reach wall. Downstream, reciprocalInvolution_continuous, reciprocalInvolution_preserves_cost, reciprocalInvolution_iterate_even, and reciprocalInvolution_never_reaches establish that the map is continuous, spends no recognition cost anywhere, has period-two orbits, and from any nonzero strain never tends to the carrier. Those facts feed the two wall theorems: kernel_cost_content_does_not_entail_cost_spending (kernel cost content holds while this continuous map fails the residue) and no_kernel_derivation_of_residue (the implication from kernel cost premises to universal cost-spending is false). The construction is not exotic: its invariance is exactly the reciprocity premise that forces $J$ in the first place (T5 / RCL lineage). It therefore separates cost law from motion law inside the gravity seven-gaps stack and motivates naming cost-spending as an explicit postulate rather than a kernel corollary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.