two_toRat
plain-language theorem explainer
The canonical ratio-orbit constant for two displays as the rational number 2. Gauge-orbit and native-cost arguments cite it whenever they evaluate a cost or trace at orbit two (nondegeneracy, vanishing, cost-display identities). The proof unfolds the ratio-orbit and toRat definitions, then closes by simp on the integer and natural transport lemmas.
Claim. The ratio-orbit constant $\mathrm{two}$ satisfies $\mathrm{toRat}(\mathrm{two}) = 2$ in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, finite distinction orbits are the inductive type DistinctionNat (K2.12). Signed differences of those orbits form SignedOrbit (K4.6: intended meaning pos − neg). A RatioOrbit (K4.7) packages an integer numerator over a nonzero orbit denominator.
The verifier map toRat sends a ratio orbit to a rational by (num.toInt : ℚ) / (den.toNat : ℚ). Spec tag A5 records that this is a transport wrapper whose internal characterization is cross-multiplication. The constant two is the ratio-orbit built from the orbit of two over the unit orbit; sibling lemmas twoOrbit_toNat and one_toNat fix the natural values of those pieces.
Upstream, ofOrbit_toInt states that a pure positive signed orbit transports to the same integer as its underlying natural, and one_toNat is the unit case one.toNat = 1.
proof idea
Term-mode proof by unfolding. Unfold the definition of the constant two and of RatioOrbit.toRat, exposing a quotient of a signed-orbit integer by a distinction-natural. Then simp with three transport facts: twoOrbit_toNat (the two-orbit is natural 2), SignedOrbit.ofOrbit_toInt (pure positive signed orbits keep their natural value as an integer), and DistinctionNat.one_toNat (the unit orbit is natural 1). The resulting rational is exactly 2.
why it matters
Orbit two is the standard probe point for native costs on ratio orbits. Downstream, cost_display rewrites the cost at any ratio as half the rational trace minus one and inserts two_toRat when simplifying the doubled-trace algebra. The vanishing and charging cluster (vanishes_at_two_iff_trace_two, vanishes_at_two_iff_flat, charges_positively_at_two, strict_somewhere_iff_charges_at_two, charges_at_two_iff_not_signGauge) all evaluate (F two).toRat and therefore depend on this identity to connect cost zero at two with the degenerate trace value 2 and with the sign-gauge inhabitant.
In the broader Recognition framework this is the discrete stand-in for evaluating the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) at the self-similar point $x=2$, which separates the flat sign cost from every nondegenerate ledger cost. It is pure foundation plumbing: no open scaffold, just the simp fact that lets the gauge-orbit classification talk about the number 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.