PRCRealRatioCharacter
plain-language theorem explainer
A real-valued character on ratio orbits: unital, multiplicative and reciprocal on nonzero ratios, never zero there, and at least 1 on positive integer orbits. Cost theorists cite it as the interface that anchor-free native costs must factor through. It is a pure Prop structure (five field axioms), not a proved theorem.
Claim. A map $\chi : \mathrm{RatioOrbit} \to \mathbb{R}$ is a real ratio character when $\chi(1)=1$; $\chi(xy)=\chi(x)\chi(y)$ and $\chi(x^{-1})=\chi(x)^{-1}$ whenever the rational displays of $x,y$ are nonzero; $\chi(x)\neq 0$ on those same nonzero orbits; and $\chi(n)\ge 1$ for every positive integer orbit $n\ge 1$.
background
Ratio orbits are the PRC display of rationals: an integer numerator over a nonzero distinction-nat denominator, with total reciprocal sending zero to zero as in $\mathbb{Q}$. The map natOrbit embeds ordinary naturals as positive integer orbits via the rational embedding.
This module sits in the cost layer that factors native ledger costs through real characters, without the two-point calibration anchor. Upstream, the Recognition Composition Law (RCL) and the related d'Alembert identity for doubled traces already constrain native costs; the CostAlgebra side supplies the multiplicative and reciprocal structure of $J$-automorphisms on positive reals as the continuum model of the same axioms.
The sibling pack SansAnchorHypotheses bundles reciprocal invariance, normalization invariance, canonical RCL, sign-reversal, monotonicity on positive integer orbits, and zero-calibration of the doubled trace. The character structure below is the real-valued factorization interface those hypotheses are meant to produce.
proof idea
No proof body: this is a Prop-valued structure (five named fields). Inhabitation is discharged elsewhere by exhibiting a concrete candidate and checking each field. The main discharge is realCharacterCandidate_is_character, which builds the candidate from a SansAnchorHypotheses pack and fills unit, multiplicativity, reciprocity, nonzeroness, and the principal-on-positive-integers bound via the corresponding candidate lemmas.
why it matters
This is the corrected factorization target's character interface. Downstream, SansAnchorRealCharacterFactorizationTarget asserts that every anchor-free native cost $F$ admits some $\chi$ satisfying these axioms together with a positive-ray factorization of $F$. The theorem realCharacterCandidate_is_character shows the concrete candidate meets the interface, and structural_sansAnchor_realCharacterFactorization lifts the same conclusion to the structural sans-anchor hypothesis pack used outside this module.
In the Recognition chain this sits under cost uniqueness and the RCL (the functional equation forcing $J$), supplying the real character through which gauge-orbit and exponent steps fire once traces at small bases are rational. It deliberately drops the two-point anchor, so factorization is stated in the weaker, anchor-free regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.