character_display
plain-language theorem explainer
A PRC ratio character is well-defined on rational displays: equal orbit displays stay equal after applying the character. Anyone extracting integer arithmetic from a factorized native cost, or proving anchor gauge rigidity, cites this. The proof is a short term composition of display/cross-equivalence transport with the canonical character cross-equivalence lemma.
Claim. Let $\chi$ be a PRC ratio character on ratio orbits. If $a,b$ are ratio orbits with equal rational displays, then the displays of $\chi(a)$ and $\chi(b)$ are equal: $a^{\mathrm{rat}}=b^{\mathrm{rat}}$ implies $(\chi a)^{\mathrm{rat}}=(\chi b)^{\mathrm{rat}}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator. Its verifier display toRat is the corresponding rational; equality of displays is equivalent (by cross-multiplication) to the internal cross-equivalence relation on orbits.
A PRC ratio character is a structured map on ratio orbits used to build native costs. In this ledger, factorized costs are often written as a character followed by a fixed J-style cost on the displayed rational (the jq family). For the induced data on positive integers to be well-defined, the character must ignore the choice of orbit representative for a given rational.
The module is the structural ledger for PRC native costs: monotone factorized costs, their multiplicative traces on naturals, and gauge rigidity of the cost anchor. Upstream, crossDisp/dispCross transport between cross-equivalence and display equality; the uniqueness layer supplies that characters respect cross-equivalence once normalize-ratio is canonical.
proof idea
Term-mode, three steps composed. dispCross turns equal rational displays into a cross-equivalence of the input orbits. That equivalence, the character hypothesis, and the proved canonical normalize-ratio target are fed to PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical, which returns a cross-equivalence of the character images. crossDisp reads that back as equality of rational displays. No further case analysis.
why it matters
Direct input to monoMult_of_character, which builds the monotone multiplicative arithmetic a factorized native cost leaves on the positive integers, and to structural_gauge_rigidity: two monotone costs that factor through characters and agree at the single orbit 2 agree on every positive integer orbit. Downstream phrasing: the anchor is a real choice and the only one (free-side stratification, form forced and unit free). Without display-invariance of characters, the induced map on naturals would not be well-defined and the uniqueness-of-anchor argument would not close. This is ledger infrastructure under the native-cost uniqueness path, not a T5–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.