absValueCharacter_prime_identity
plain-language theorem explainer
On every prime distinction orbit, the absolute-value character returns a ratio orbit cross-equivalent to the prime direction itself. Native-cost uniqueness arguments cite this to calibrate the character on primes and to discharge orientation coherence. The proof rewrites cross-equivalence as rational equality and uses nonnegativity of the prime's natural display.
Claim. For every prime distinction-orbit $p$, writing $d_p$ for its prime direction, the absolute-value character of $d_p$ is cross-equivalent to $d_p$: the scaled numerators balance under the internal ratio-orbit relation, equivalently their rational displays agree.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (the internal stand-in for $\mathbb{N}$). A prime orbit is a distinction-nat that is prime in the orbit-divisibility sense. Ratio orbits package a signed numerator over a nonzero distinction denominator; they are the internal rational displays of the calculus.
Cross-equivalence of two ratio orbits means the scaled numerators balance as signed orbits (a.num scaled by b.den balances b.num scaled by a.den). Upstream, this is proved equivalent to equality of the verifier rationals: cross-multiplication agrees with rational equality of the displays.
The absolute-value character is the candidate multiplicative character used to build native cost from ratio data. Prime directions are the distinguished ratio-orbit directions attached to prime orbits. This lemma sits in the native-cost uniqueness module, where characters are constrained on primes before global uniqueness is assembled.
proof idea
Term-mode after intro p hp. Rewrite the goal with three facts: cross-equivalence iff rational displays agree; the absolute-value character's rational display; and the prime direction's rational display. The residual goal is $|q|=q$ for the rational image of the prime direction. Discharge by abs_of_nonneg, using that the underlying natural (p.toNat) is nonnegative (via the arithmetic-from-logic zero bound, cast into $\mathbb{Q}$).
why it matters
Native-cost uniqueness needs the absolute-value character to act as the identity on prime directions, both for calibration and for orientation coherence. Downstream, absValueCharacter_prime_calibrated lifts this identity through ratio-orbit congruence to the calibrated-prime-direction predicate, and absValueCharacter_prime_orientation_coherent takes the left disjunct of orientation coherence directly from this theorem.
In the broader Recognition stack this is foundation plumbing under the J-cost and forcing chain: characters on ratio orbits must match the native cost before uniqueness of the cost functional (and later T5 J-uniqueness) can be stated in PRC-native language. It closes a concrete prime-case obligation rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.