recip_generates_cost_and_scale
plain-language theorem explainer
The reciprocal map on the positive reals is the shared generator of both recognition-cost symmetry and the golden-ratio scale. Cite this when the math/physics bridge must rest on one involution rather than a glued pair of unrelated facts. J is invariant under inversion, and φ is the unique fixed point greater than 1 of the shifted reciprocal. The proof is a term-mode pairing of the two component lemmas already proved in the module.
Claim. For every real $x > 0$, the recognition cost satisfies $J(x^{-1}) = J(x)$. Moreover, for every real $x > 1$, one has $1 + x^{-1} = x$ if and only if $x = \varphi$ (the golden ratio).
background
This module isolates the reciprocal involution $\iota(x) = x^{-1}$ on the positive reals as the common structural object beneath both sides of the Recognition bridge. Unlike the assembly in OneLaw, which conjoins facts about unrelated objects, both halves here quantify over the same map.
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). Its defining algebraic feature is $\iota$-symmetry: $J \circ \iota = J$. The scale side uses the affine shift $g(x) = 1 + \iota(x)$; the golden ratio $\varphi$ is forced as the unique fixed point of $g$ strictly above 1 (framework landmark T6).
Upstream, the component facts are already available: $J$-symmetry under reciprocal, and the fixed-point characterization of $\varphi$ for the shifted reciprocal. The present declaration packages them as a single conjunction about one generator.
proof idea
Term-mode proof by pairing. The first conjunct is discharged by applying the already-proved lemma that $J(\mathrm{recip}, x) = J(x)$ for $x > 0$. The second conjunct is discharged by applying the already-proved fixed-point equivalence: for $x > 1$, $\mathrm{recipShift}, x = x$ if and only if $x = \varphi$. No further algebra is performed; the constructor simply conjoins the two lemmas.
why it matters
In the Recognition forcing chain, T5 pins $J$ as the unique cost of the stated shape, and T6 forces $\varphi$ as the self-similar scale. This theorem states the sharpest common-generator form of that bridge: one involution family supplies both the symmetry axis of $J$ (fixed point of $\iota$ is the unit, which is $J$'s null point) and the defining equation of $\varphi$ (fixed point of $1 + \iota$).
The module doc contrasts this with a mere assembly of independent facts. Here both conjuncts range over the same reciprocal, so the involution is logically upstream of cost symmetry and of the golden-ratio equation. Downstream use is not yet wired in the graph (used-by count zero), but sibling certificates in the module (recip_pins_unit_and_scale, the reciprocal-generator certificate) are the natural consumers for framework-level packaging.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.