realCharacterCandidate_unit
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real character candidate extracted from a ratio-orbit map F sends the unit orbit to 1. Anyone building a PRC real ratio character from the doubled-trace factorization cites this unit law. The proof is a two-branch case split on whether the doubled trace at 2 is degenerate, then simp with the corresponding unit lemmas.
Claim. Let $F$ be a map on ratio orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace). Then the real character candidate built from $F$ evaluates to $1$ at the unit ratio orbit.
background
In the real-character factorization module, a native cost on ratio orbits is packaged without an external anchor via SansAnchorHypotheses: base-sans-two structure, sign-reversal, monotonicity, and zero-calibration of the doubled trace. From such an $F$ one forms the doubled trace as a real-valued function on rational displays (rationalTrace), then extracts a candidate real character on ratio orbits.
The candidate is defined by cases: if rationalTrace F 2 = 2 (degenerate anchor), it collapses to the rational sign character; otherwise it uses a generalized linear extraction from the nontrivial root data, with a zero clause at the zero display. The unit ratio orbit satisfies one.toRat = 1.
Upstream, the nontrivial branch already knows that the extracted nontrivial character value at $1$ is $1$ (via linear extraction at the unit, using nonvanishing of the anchor root and of its square-minus-one). The sign character is trivially $1$ at $1$.
proof idea
Case-split on whether rationalTrace F 2 = 2.
- Degenerate branch: unfold the candidate definition, use
one.toRat = 1, and applyrationalSignCharacter_oneto get $1$. - Nondegenerate branch: same unfold and
one.toRat = 1, then applynontrivialCharacterValue_one(which needs the SansAnchor pack and the nondegeneracy hypothesis) to conclude the nontrivial extraction at $1$ is $1$.
Both branches finish by simp.
why it matters
This is the unit axiom in the bundle that promotes the candidate to a full PRC real ratio character. Downstream, realCharacterCandidate_is_character assembles unit, multiplicativity, and reciprocity; its unit field is exactly this theorem.
In the Recognition cost story, characters on ratio orbits are the bridge from native doubled-trace data (tied to the J-cost / RCL lineage and PRC uniqueness) to a real multiplicative character usable in cost-from-character reconstructions. Establishing the unit law is the first structural check that the case-split extraction is not an ad-hoc display map but a genuine character at the identity.
It does not by itself force uniqueness of the cost or pin physical constants; it closes the unit slot so the character interface can be used further in the factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.