half_toRat
plain-language theorem explainer
The ratio-orbit constant built as one-half displays as the rational 1/2. Anyone evaluating PRC's rational J-cost on ratio orbits cites this simp lemma. The proof unfolds the half constructor and the toRat display, then discharges with the orbit-to-nat and signed-orbit-to-int bridges.
Claim. The ratio-orbit object representing one-half evaluates under the rational display map to $1/2 \in \mathbb{Q}$.
background
Primitive Recognition Calculus builds rationals from distinction orbits before any real analysis. A DistinctionNat is a bare counting orbit; a SignedOrbit is an intended difference pos − neg; a RatioOrbit is an integer numerator over a nonzero orbit denominator (K4.6–K4.7).
The display map toRat sends a ratio orbit to an ordinary rational by converting numerator and denominator through toInt/toNat. The constant half is the ratio-orbit encoding of $1/2$, built from the two-orbit and the unit distinction.
This module equips those ratio orbits with PRC's rational J-cost object $J(q)=((q+q^{-1})/2)-1$, the same algebraic skeleton as the unique cost forced later on the reals (T5). The present lemma is the constant-evaluation step for the factor $1/2$ inside that formula.
proof idea
Term-mode proof by unfolding. Unfold the definition of half and of RatioOrbit.toRat, exposing the numerator/denominator conversion. Then simp with three bridges: twoOrbit_toNat (the two-orbit displays as 2), SignedOrbit.ofOrbit_toInt (a pure positive orbit converts to its natural as an integer), and DistinctionNat.one_toNat (the unit distinction is 1). The resulting arithmetic identity is $1/2$.
why it matters
Direct dependency of onRatioOrbit_toRat, which states that the PRC rational J-cost on any ratio orbit $q$ satisfies
$(J(q)).\mathrm{toRat}=(q.\mathrm{toRat}+q.\mathrm{toRat}^{-1})/2-1$.
That parent rewrites through half_toRat (together with add/mul/recip/one display lemmas) and closes by ring.
In the Recognition forcing chain this is the discrete, rational-level realization of the J skeleton $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) before the real-analytic uniqueness theorem (T5) is bridged. Without the half constant evaluating correctly, the rational J-cost object cannot match the classical formula on $\mathbb{Q}_{>0}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.