costFromCharacter_div_congr
plain-language theorem explainer
For a ratio-orbit character χ, the native cost of a quotient orbit x/y built from χ is cross-equivalent to the orbit display of χ(x)/χ(y). Anyone proving that character-derived PRC costs obey the Recognition Composition Law cites this. The proof unfolds the cost and division maps, then chains multiplicativity of χ on (x, recip y) with reciprocity of χ via cross-equivalence transitivity.
Claim. Let $\chi$ be a ratio-orbit character: unit-preserving, multiplicative, and reciprocal up to cross-equivalence on ratio orbits. Then for all ratio orbits $x,y$, the character-cost of the quotient satisfies $\mathrm{cost}_\chi(x/y)\,\sim_\times\,\mathrm{display}(\chi(x)/\chi(y))$, where $\sim_\times$ is cross-multiplication equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, positive ratios live as RatioOrbit objects (δ-orbit numerators and denominators). Equality is not definitional: two orbits are related by crossEq when cross-multiplication balances as signed orbits (K4.10), the internal PRC rational relation.
A PRCRatioCharacter χ is a map on ratio orbits that is unit-preserving, multiplicative, and reciprocal, all up to crossEq rather than definitional equality, so the structure stays quotient-native. The native cost built from such a character, costFromCharacter, sends an orbit through χ and then to the cost display on the orbit level.
Division of orbits is multiplication by the reciprocal orbit. Upstream, crossEq is reflexive and transitive (choice-free via the integer bridge), and character axioms supply the multiplicative and reciprocal legs used here.
proof idea
Term proof. Unfold costFromCharacter and div (division as mul-by-reciprocal). The goal reduces to a congruence of the orbit display under onRatioOrbit_congr.
Build the needed crossEq by crossEq_trans: first apply character multiplicativity at (x, recip y), so χ(x · y⁻¹) matches χ(x) · χ(y⁻¹); then apply ratioOrbit_mul_congr to the pair (crossEq_refl (χ x), hχ.reciprocal y), replacing χ(y⁻¹) by (χ y)⁻¹. The composite is exactly the display of χ(x)/χ(y).
why it matters
This is the division-compatibility lemma for character-derived native costs. Its sole downstream consumer is costFromCharacter_canonical_rcl, which assembles the full Recognition Composition Law identity
$J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$
at the ratio-orbit level for costs built from a PRC ratio character.
In the Recognition framework that step is the algebraic content of T5 (J-uniqueness) and the RCL landmark: once costs factor through a character with unit, multiplicative, and reciprocal axioms, the d'Alembert/RCL form is forced. The lemma closes the quotient leg so the canonical RCL theorem can treat mul and div symmetrically without leaving the cross-equivalence quotient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.