realCharacterCandidate
plain-language theorem explainer
Extracts a real-valued multiplicative character on ratio orbits from a cost map F by reading the doubled trace at the anchor 2. When that trace is degenerate (equals 2), the candidate is the sign character; otherwise it uses nondegenerate linear extraction, returning zero at zero. Factorization and gauge-orbit theorems cite this as the character that rebuilds the cost. The body is a three-way case split on the anchor value and the rational display of the orbit.
Claim. Given a map $F$ on ratio orbits and an orbit $q$, define a real number by cases: if the doubled trace of $F$ at $2$ equals $2$, return the sign of the rational display of $q$ (zero at zero); if that display is zero, return $0$; otherwise return the nondegenerate linear extraction of the doubled trace of $F$ at the rational display of $q$.
background
In the real-character factorization module, cost maps act on ratio orbits: each orbit is an integer numerator over a nonzero orbit denominator, with a verifier display toRat sending the orbit to an ordinary rational. The doubled trace of such a map $F$ is the real-valued function on rational displays obtained by evaluating the trace display of $F$ on the orbit of that rational.
Two extraction routes sit upstream. The rational sign character is $+1$ on positives, $-1$ on negatives, and $0$ at zero. The nondegenerate value is the linear extraction of the doubled trace against the anchor root of $F$, applied at a nonzero rational. The present definition chooses between those routes by testing whether the doubled trace of $F$ at the anchor $2$ is the degenerate value $2$.
The local setting is the reconstruction of a real multiplicative character from a native cost so that the cost can be recovered as a function of that character (the cost-from-character construction used later in the module).
proof idea
Pure definition by nested case split, not a proof. First compare the doubled trace of $F$ at $2$ with $2$. On equality, return the rational sign character of the verifier display of $q$. Otherwise, if that display is zero, return $0$; else return the nondegenerate character value of $F$ at the display. No lemmas are applied; the branches simply name the two upstream extractors and the zero clause.
why it matters
This is the character object that the factorization theorems package. Under the sans-anchor hypotheses it is proved to be a PRC real ratio character (unit, multiplicative, reciprocal), and the cost of $F$ on positive orbits agrees with the cost rebuilt from this character. Multiplicativity and nonvanishing lemmas are stated directly for it.
Downstream, the gauge-orbit module specializes to the sign-gauge native cost: the candidate collapses exactly to the sign character, has character exponent zero, and is not any positive odd integer power at the anchor orbit of $2$. Those facts pin the degenerate branch of the factorization and separate the sign gauge from nontrivial power characters.
In the broader Recognition cost story, the construction isolates the real character factor of a native cost after the doubled-trace / d'Alembert analysis, so later uniqueness and gauge results can quote a single real-valued map rather than the full orbit map $F$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.