realCharacterCandidate_is_character
plain-language theorem explainer
Under the anchor-free native-cost hypotheses on an orbit map F, the extracted real-valued candidate is a principal ratio character: unital, multiplicative on nonzero orbits, reciprocal, nowhere zero on nonzero orbits, and principal on positive integers. Cost-factorization arguments cite this to package the candidate as a genuine character. The proof is a structure assembly from five previously proved field lemmas.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base without two, sign-reversing, monotone, and zero-calibrated doubled trace). Then the real character candidate $\chi_F$ extracted from the doubled trace of $F$ is a principal real ratio character: $\chi_F(1)=1$, $\chi_F(xy)=\chi_F(x)\chi_F(y)$ and $\chi_F(x^{-1})=\chi_F(x)^{-1}$ whenever the rational representatives are nonzero, $\chi_F(x)\neq 0$ on nonzero orbits, and $\chi_F$ is principal on the positive-integer orbit.
background
This module builds an anchor-free real character factorization for native costs on ratio orbits. A ratio orbit is an equivalence class of rational scale factors; the native cost map $F$ acts on those orbits. The doubled trace of $F$ is the real-valued functional obtained by evaluating the cost along a two-sided orbit and symmetrizing.
SansAnchorHypotheses packages the structural assumptions used in place of a fixed two-anchor: the base omits the special role of two, $F$ is sign-reversing and monotone in the native-cost sense, and the doubled trace is zero-calibrated. From those data one defines realCharacterCandidate, which is the ordinary rational sign character when the doubled trace at two equals two, and otherwise a generalized linear extraction from the doubled trace (with value zero on the zero orbit).
A PRCRealRatioCharacter is a real-valued map on ratio orbits that is unital, multiplicative and reciprocal on nonzero orbits, nowhere zero there, and principal on the positive-integer orbit. The algebraic CostAlgebra layer supplies the ambient multiplicative and reciprocal structure that these character axioms mirror.
proof idea
Term-mode structure construction. Each field of PRCRealRatioCharacter is discharged by a named lemma already proved for the candidate under the same hypotheses:
- unit from
realCharacterCandidate_unit; - multiplicativity from
realCharacterCandidate_mul(applied at nonzero rational representatives); - reciprocity from
realCharacterCandidate_recip; - nonvanishing from
realCharacterCandidate_nonzero; - principality on the positive-integer orbit from
realCharacterCandidate_principal_on_pos_int.
No further calculation occurs in this declaration; it only packages those five results into the character structure.
why it matters
This is the character-existence half of the anchor-free factorization. The sole downstream consumer is SansAnchorRealCharacterFactorizationTarget_proved, whose doc-comment states that "the anchor-free doubled trace always factors through a real-valued principal character." That target packages the candidate, this character proof, cost agreement, and small-trace rationality into one existence statement.
In the Recognition framework the native cost is forced by the Recognition Composition Law and J-uniqueness (T5: $J(x)=(x+x^{-1})/2-1$). Factoring the doubled trace through a real principal character is the bridge from that abstract cost to a concrete multiplicative character on ratio orbits, which is what later mass-ladder and coupling extractions read off. Closing the sans-anchor path removes dependence on a distinguished two-point calibration while retaining the same character calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.