realCharacterCandidate_mul
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real character extracted from the doubled trace is multiplicative on nonzero ratio orbits. Anyone assembling a PRC real ratio character from a native cost map cites this. The proof splits on whether the doubled trace at 2 is degenerate (sign character) or nontrivial, and reduces each branch to an already-proved multiplicativity lemma.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost pack (base-sans-two, sign-reversing, monotone, zero-calibrated doubled trace). For ratio orbits $x,y$ with nonzero rational displays, the real character candidate of $F$ obeys $\chi_F(x\cdot y)=\chi_F(x)\,\chi_F(y)$.
background
This module builds a real multiplicative character from a native cost map $F$ on ratio orbits (signed rational displays). The doubled trace is promoted to an honest function rationalTrace on $\mathbb{Q}$; the real character candidate is then defined by cases: if $\mathrm{Tr}_F(2)=2$ (degenerate anchor), use the rational sign character; otherwise extract a nontrivial character value from the doubled trace, sending the zero display to $0$.
SansAnchorHypotheses packages the structural assumptions matching the PRC native-cost pack without an external anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Multiplicativity of the orbit product on rational displays is mul_toRat: $(x\cdot y).\mathrm{toRat}=x.\mathrm{toRat},y.\mathrm{toRat}$.
Upstream, multiplicativity is already known separately for the two branches: the rational sign character is multiplicative on $\mathbb{Q}$, and nontrivialCharacterValue_mul gives multiplicativity of the nontrivial extraction when $\mathrm{Tr}_F(2)\neq 2$.
proof idea
First record that the product of the two nonzero rational displays is nonzero. Case-split on whether $\mathrm{Tr}_F(2)=2$.
Degenerate branch: unfold the candidate definition; the if reduces to the rational sign character, and rationalSignCharacter_mul plus mul_toRat finish by simplification.
Nontrivial branch: the same unfold hits the else arm; after rewriting the product display via mul_toRat and discharging the three nonzero guards, the goal is exactly nontrivialCharacterValue_mul applied to the SansAnchor pack and the nontriviality hypothesis.
why it matters
This is the multiplicativity leg of the character package. Downstream, realCharacterCandidate_is_character assembles a full PRCRealRatioCharacter instance by combining unit, multiplicativity (this theorem), and reciprocal laws. That instance is the bridge from native cost data to a real ratio character, which feeds cost-from-character constructions in the same module.
In the Recognition framework the cost side is pinned by T5 J-uniqueness and the Recognition Composition Law; extracting a genuine multiplicative character from the doubled trace is the algebraic step that lets native cost data act as a homomorphism on ratio orbits rather than a mere functional equation solution. Closing multiplicativity without an external anchor keeps the forcing chain free of ad-hoc basepoint choices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.