two
plain-language theorem explainer
The rational orbit display for the integer 2, written as the fraction 2/1 in the primitive recognition calculus. Anyone citing native constants in cost algebra, RCL identities, or action functionals needs this witness. It is a pure structure packing: lift the two-step distinction orbit to a nonnegative signed numerator over the unit denominator.
Claim. The rational orbit equal to $2/1$: numerator is the nonnegative signed orbit of the two-step distinction position, denominator is the unit distinction orbit (with the unit nonzero).
background
Primitive recognition calculus builds numbers from repeated distinction before any base or field structure. DistinctionNat is the base-neutral finite orbit of successive distinctions (zero, successor). The two-step position is simply the successor of one.
A signed orbit is an ordered pair of distinction positions, read as a difference pos − neg. Nonnegative integers embed by taking the negative part to be zero. A ratio orbit (K4.7) is then an integer numerator over a nonzero distinction denominator: the native display of a rational before real embedding.
This module sits under the J-cost development: the unique cost forced by the Recognition Composition Law is later evaluated on such ratio orbits. The constant two is the first nontrivial integer beyond the unit and appears in every doubled term of the RCL.
proof idea
Definitional structure construction, not a proof. Pack three fields of a ratio orbit: numerator is ofOrbit applied to the two-step distinction position (nonnegative signed orbit with zero negative part); denominator is the unit distinction orbit; the nonzero witness is the already-proved fact that one ≠ zero.
why it matters
Supplies the native constant 2 used across the cost and action layers. Downstream, CostAlgebra cites it in the Recognition Composition Law identity, in the classification that every J-automorphism is identity or reciprocal (via evaluation at two), and in defect-distance quasi-triangle counterexamples. Action-side consumers include pointwise convexity of Jcost, geodesic minimization via convexity, and the Hessian geodesic equation.
In the forcing chain, T5 fixes J(x) = (x + x⁻¹)/2 − 1; the explicit factor 2 in that formula and in the RCL is this orbit once reals are attached. Without a first-class native two, later uniqueness and convexity arguments would smuggle an external numeral.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.