character_one_toRat
plain-language theorem explainer
Any PRC ratio character sends the unit ratio orbit to a ratio orbit whose rational display equals 1. Used when normalizing characters before multiplicative and reciprocal display lemmas, and before trace/cost rigidity. Proof is a short transport: the native unit field, cross-multiplication iff rational equality, then the unit display simp.
Claim. Let $\chi$ be a PRC ratio character (a structure-preserving map on ratio orbits). Then the rational display of $\chi(1)$ equals $1$: $(\chi(1)).\mathrm{toRat} = 1$.
background
Ratio orbits are the native rational display in the Primitive Recognition Calculus: a signed-orbit numerator over a nonzero distinction-nat denominator. The verifier map toRat sends such an orbit to $\mathbb{Q}$ by integer division; equality of displays is characterized by cross-multiplication (crossEq), not by raw structural identity.
A PRC ratio character is a map $\chi$ on ratio orbits carrying the native multiplicative/unit axioms used for cost uniqueness. Its unit field asserts that $\chi$ fixes the unit orbit up to cross-equality. The module sits in the continuum character-rigidity forcing layer, imported from native cost uniqueness, and prepares display-level normalizations before calibrated-character and trace-rigidity results.
Upstream, crossEq_iff_toRat_eq states that cross-multiplication agrees with rational equality of verifier displays; one_toRat is the simp fact that the unit orbit displays as $1$.
proof idea
Term-style rewrite chain. Extract the character's native unit axiom (hχ.unit), which gives cross-equality of $\chi(1)$ with the unit orbit. Rewrite that hypothesis by crossEq_iff_toRat_eq to obtain equality of rational displays. Finish by rewriting with one_toRat, so the right-hand side becomes $1$. No induction or case split.
why it matters
Unit normalization is the base calibration step for characters on the rational display. Sibling lemmas in the same module lift multiplicativity and reciprocity to toRat, then build calibrated characters and force rigidity of the doubled trace and of the cost reconstructed from a character. That rigidity line is how PRC pins the native cost against continuum displays, feeding the uniqueness story behind the Recognition Composition Law and the J-cost (T5) rather than an ad hoc continuum ansatz.
No downstream edges are recorded yet; the declaration is infrastructure inside CharacterRigidityForcing, not a leaf cited from outside the module. It closes the unit case so later rigidity theorems can assume a character already displays as $1$ at the identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.