recip_one_crossEq_one
plain-language theorem explainer
The reciprocal of the unit ratio-orbit is cross-equivalent to the unit itself: internally, 1^{-1} balances 1. Order and rational-display lemmas in the Primitive Recognition Calculus cite this as the base case that the unit is fixed by inversion. The proof rewrites cross-equivalence to rational equality, applies the reciprocal and unit display lemmas, and finishes by numeric normalization.
Claim. Under the internal ratio-orbit cross-multiplication relation, $\mathrm{recip}(1)$ is equivalent to $1$: the reciprocal of the unit ratio-orbit balances the unit ratio-orbit.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of such displays is not raw structural equality; it is the internal relation crossEq, which asserts that the two cross-products of numerators and denominators balance as signed orbits (K4.10). That relation is designed to match ordinary rational equality of the verifier displays.
The total reciprocal on ratio orbits sends a zero numerator to zero and otherwise swaps numerator and denominator in the nonzero case (K4.12). The unit ratio-orbit displays as the rational $1$. Together these give a native calculus of rationals built only from $\delta$-orbit positions, before any external $\mathbb{Q}$ is assumed as primitive.
Upstream, crossEq_iff_toRat_eq states that cross-multiplication agrees with equality of the rational displays; recip_toRat states that the display of a reciprocal is the field inverse of the display; and one_toRat is the simp fact that the unit displays as $1$.
proof idea
Short tactic proof. Rewrite the goal with crossEq_iff_toRat_eq, turning cross-equivalence into equality of rational displays. Then rewrite with recip_toRat and one_toRat, so the goal becomes $(1)^{-1} = 1$ in $\mathbb{Q}$. Close by norm_num.
why it matters
This is the unit fixed-point fact for inversion inside the integer/rational order surface of PRC. The immediate sibling one_crossEq_recip_one is just the symmetric form via crossEq_symm. Both feed the closed certificate integer_order_certificate, whose doc-comment states that the internal signed-orbit order surface is closed: display lemmas for truncated subtraction, $\le$, absolute difference, and nonnegativity flags are packaged together.
In the broader Recognition stack this sits under Foundation, before the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It does not itself force $\varphi$ or the cost $J$; it only seals that the native unit behaves as $1^{-1}=1$ under the internal rational relation, so later order and cost constructions can treat the unit without a special case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.