canonicalSelectedNativeCost_native_hypotheses
plain-language theorem explainer
The canonical native cost on ratio orbits satisfies the five base native-cost axioms: reciprocal symmetry, normalization invariance, the Recognition Composition Law, unit-zero, and two-calibration. Anyone building uniqueness or minimality certificates for the PRC cost will cite this packing lemma. The proof reduces each field to rational arithmetic via the toRat display and finishes by field_simp/ring.
Claim. The canonically selected native cost $C$ on ratio orbits satisfies the base native-cost hypothesis package: $C(q^{-1})=C(q)$ (reciprocal symmetry); $C$ is invariant under ratio normalization; $C$ obeys the Recognition Composition Law $C(xy)+C(x/y)=2C(x)C(y)+2C(x)+2C(y)$ on nonzero rationals; $C(1)=0$; and $C$ is calibrated at the orbit of $2$.
background
In the Primitive Recognition Calculus, costs are evaluated on ratio orbits (integer-rational pairs with a signed numerator/denominator display). Equality of costs is witnessed by cross-multiplication, which is equivalent to equality of the rational displays (crossEq_iff_toRat_eq). The selected witness canonicalSelectedNativeCost is the discrete stand-in for the continuous J-cost $J(x)=(x+x^{-1})/2-1$ forced at T5 of the unified forcing chain.
The base native-cost hypothesis class packages five structural demands: reciprocal symmetry under orbit inversion, invariance under the distinction-nat normalizer, the Recognition Composition Law (RCL) on the orbit algebra, vanishing at the unit orbit, and a fixed calibration value at the orbit of two. Upstream arithmetic lemmas (add_toRat, mul_toRat, recip_toRat, normalizeRatio_toRat) transport these identities from $\mathbb{Q}$ back to the orbit layer.
The module sits in the foundation spine that selects a unique native cost before minimality and uniqueness certificates are issued.
proof idea
Five structure fields are discharged separately.
- Reciprocal: rewrite both sides via
crossEq_iff_toRat_eqandcanonicalSelectedNativeCost_toRat, applyrecip_toRat, then case on whether the rational display is zero (simp) or not (field_simp+ring). - Normalized invariant: same crossEq/toRat bridge, then
DistinctionNat.normalizeRatio_toRat. - Canonical RCL: expand addition and multiplication of orbits to rationals (
add_toRat,mul_toRat,div_toRat,two_toRat), clear nonzero denominators withfield_simp, finish byring_nf. - Unit zero: unfold the selected cost and hit the
if_posbranch at the unit orbit (one_toRat). - Two-calibrated: direct appeal to the already-proved crossEq identity of the selected cost on the orbit of two.
why it matters
This is the base packing step that makes the selected witness a legitimate native cost before any strengthened or minimality claims. Downstream, canonicalSelectedNativeCost_full_hypotheses lifts it to the full zero-calibrated prime-signed strengthened class ("the frozen ledger is non-vacuous"), and the minimality certificate path uses the same reciprocal/normalization pattern for the RCL-spike cost under slim hypotheses.
In the Recognition framework this anchors T5 J-uniqueness and the RCL identity at the discrete orbit level: once the selected cost is known to satisfy the base package, uniqueness and exclusion of degenerate competitors (constant-zero, linear) can proceed. It is the bridge from the algebraic definition of the selected witness to the non-vacuous ledger used by the public spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.