realCharacterCandidate_recip
plain-language theorem explainer
Under the anchor-free native-cost hypotheses, the real character candidate on ratio orbits sends reciprocal orbits to reciprocal reals. Anyone proving that this candidate is a genuine multiplicative character on nonzero rational displays cites it for the reciprocal axiom. The proof is a two-branch case split on whether the doubled trace at 2 is degenerate, reducing to the sign character or the nontrivial extraction reciprocity lemmas.
Claim. Let $F$ be a map on rational ratio orbits satisfying the anchor-free native-cost hypotheses (base without the two-anchor, sign-reversing, monotone, zero-calibrated doubled trace). For every ratio orbit $x$ with rational display $x\neq 0$, the real character candidate of $F$ at the reciprocal orbit equals the reciprocal of its value at $x$: $\chi_F(x^{-1})=\chi_F(x)^{-1}$.
background
In the cost factorization module, ratio orbits are rational displays: a signed numerator orbit over a nonzero distinction-nat denominator. The doubled trace of a native cost $F$ is promoted to an honest real-valued function rationalTrace on rational displays. From that trace one extracts a real-valued candidate character on ratio orbits: if the doubled trace at 2 equals 2 (degenerate anchor), the candidate is the ordinary rational sign character; otherwise it uses a nontrivial generalized-linear extraction (with a zero clause at the zero display).
SansAnchorHypotheses packages the structural native-cost assumptions without fixing an anchor: base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace. Reciprocity for the two extraction branches is already available upstream: the sign character satisfies $\mathrm{sgn}(x^{-1})=\mathrm{sgn}(x)^{-1}$ on nonzero rationals, and the nontrivial character value does likewise under the anchor-free pack when the trace at 2 is nondegenerate.
proof idea
First note that the reciprocal rational display is nonzero whenever the original is. Case on whether rationalTrace F 2 = 2.
Degenerate branch: unfold the candidate definition; both sides become the rational sign character on reciprocal displays, and rationalSignCharacter_recip finishes after rewriting the orbit reciprocal to the rational inverse.
Nondegenerate branch: the candidate reduces to the nontrivial character value (the zero clause is excluded by the nonzero hypothesis). Apply nontrivialCharacterValue_recip under the same anchor-free pack and the nondegeneracy hypothesis.
why it matters
This is one of the three field axioms needed to promote the real character candidate to a PRCRealRatioCharacter. The parent theorem realCharacterCandidate_is_character assembles unit, multiplicativity, and this reciprocal law into that structure instance, which is the bridge from native cost data to a genuine real ratio character.
In the Recognition cost story, characters extracted from the doubled trace are the algebraic objects that factor the cost and connect to the Recognition Composition Law and J-uniqueness (T5). Closing reciprocity without an anchor hypothesis keeps the factorization path aligned with the anchor-free native-cost uniqueness line rather than a special fixed point at 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.