half
plain-language theorem explainer
Defines the rational orbit display for one-half: numerator the unit distinction orbit, denominator the two-orbit. Anyone building J-cost evaluations, half-rung ladder tolerances, or reciprocal-symmetric ratios on the primitive recognition calculus cites this constant. The body is a structure instance plus a short contradiction that the two-orbit is nonzero via its natural-number image.
Claim. Let $\mathsf{half}$ be the rational orbit with numerator the nonnegative signed orbit of the unit distinction count and denominator the two-orbit (the double successor of zero). Its denominator is nonzero, so $\mathsf{half}$ is a well-formed element of the rational-orbit type and represents the ratio $1/2$.
background
In the primitive recognition calculus, finite counts are DistinctionNat orbits: zero and successor, base-neutral repeated distinction. Signed orbits package a difference of two such counts (intended meaning pos minus neg); ofOrbit embeds a nonnegative count as a signed orbit with zero negative part.
A RatioOrbit (K4.7) is an integer numerator over a nonzero orbit denominator: the display type for rationals built only from distinction data, before passage to ordinary rationals or reals. The sibling twoOrbit is the distinction orbit for two; this definition pairs the unit orbit in the numerator with that denominator.
The module sits under Foundation and imports the J-cost functional equation and Euclidean orbit geometry. Half appears as the canonical reciprocal of two once integers and rationals have been reconstructed from logic-level orbits.
proof idea
Structure instance: numerator is SignedOrbit.ofOrbit applied to the unit distinction orbit; denominator is the preexisting twoOrbit. Nonzeroness of the denominator is proved by contradiction: assume equality with zero, apply DistinctionNat.toNat (the forward map reading iteration count), rewrite with twoOrbit_toNat and toNat_zero, then norm_num obtains $2 = 0$.
why it matters
Half is a primitive constant on the rational-orbit layer that feeds dozens of downstream sites. Planetary formation uses half-rung tolerance: measured semi-major axes agree with the $\varphi$-ladder inside a $\sqrt{\varphi}$ window, "exactly half the adjacent ratio in log-space" (AgreesAtHalfRung, planetaryFormationCert). Alpha and spectral work cite half-period dimensions and half-angle identities (half_period_dim_eq, normSq_omega8_pow_sub_one with $4\sin^2(k\pi/8)$). Chemistry and curvature derivations also consume the symbol for half-filled shells and balance identities.
In the broader RS chain, rational orbits sit under the J-cost calculus (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) and the $\varphi$-ladder mass and orbital formulae. Having $1/2$ as a first-class orbit, not a smuggled real, keeps reciprocal symmetry and normalized invariants inside the foundation before any continuum embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.