nontrivialCharacterValue_one
plain-language theorem explainer
Under anchor-free native-cost hypotheses and nontriviality (doubled trace at 2 is not 2), the extracted real character equals 1 at the rational unit. Cited by anyone assembling the multiplicative character for Erdős-type classification of the ledger cost. Proof is a one-line application of the linear-extraction unit lemma with the four root and trace side conditions.
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). If the rational doubled trace of $F$ at $2$ satisfies $T_F(2)\neq 2$, then the nontrivial character value extracted from $F$ at $1$ equals $1$.
background
In the real-character factorization of the Recognition cost, one extracts a real-valued map on rational displays from the doubled ledger trace. The rational trace $T_F$ sends a rational $x$ to the doubled-trace display of the ratio orbit of $x$. The anchor root $r_F$ is the positive real solving $r+r^{-1}=T_F(2)$ (when that trace is at least 2). Linear extraction then builds a candidate character by a fixed algebraic formula in $T_F$ and $r_F$.
SansAnchorHypotheses packages the anchor-free native-cost axioms: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Nontriviality $T_F(2)\neq 2$ forces $r_F>1$, so the extraction is nondegenerate. The object nontrivialCharacterValue F x is exactly linear extraction of $T_F$ at root $r_F$ evaluated at $x$.
Upstream, anchorRoot_add_inv identifies $r_F+r_F^{-1}$ with $T_F(2)$, anchorRoot_ne_zero and anchorRoot_sq_sub_one_ne_zero supply the denominator nonvanishing, and rationalTrace_one gives $T_F(1)=2$.
proof idea
One-line term proof: apply the private lemma linearExtraction_unit to $T:=$ rational trace of $F$ and $r:=$ anchor root of $F$. The four hypotheses are discharged by rationalTrace_one hF ($T(1)=2$), anchorRoot_ne_zero hF ($r\neq 0$), anchorRoot_sq_sub_one_ne_zero hF hnontrivial ($r^2-1\neq 0$), and anchorRoot_add_inv hF ($r+r^{-1}=T(2)$). No further rewriting is needed; the unit identity for linear extraction is exactly the claim.
why it matters
This is the unit axiom for the extracted character. Downstream, natChar_monotoneMultiplicative in GaugeOrbitClassification quotes it to feed Erdős's theorem: the positive-integer restriction is completely multiplicative and monotone, with unit supplied by this result. Sibling lemmas nontrivialCharacterValue_recip, _pow, and _nonzero build the rest of the character calculus on the same extraction, and realCharacterCandidate_unit uses the same unit fact in the degenerate/nondegenerate case split.
In the Recognition framework the cost $J$ is forced unique by T5 (J-uniqueness via the Recognition Composition Law). Factoring the real character of the native cost is the bridge from that abstract uniqueness to concrete multiplicative classification on orbits. Without the unit identity, the Erdős hypotheses package does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.