structural_sansAnchor_realCharacterFactorization
plain-language theorem explainer
Every anchor-free structural native cost F on ratio orbits factors as the classical J-cost of a real multiplicative character χ. Anyone classifying gauge orbits or proving the signed-power family will cite this. The proof is a one-line term that packages structural ledger hypotheses into the light SansAnchor pack and applies the already-proved real-character factorization target.
Claim. Let $F$ map ratio orbits to ratio orbits and satisfy the structural anchor-free native-cost hypotheses (base-sans-two reciprocity, sign-reversing, monotone, zero-calibrated doubled trace). Then there exists a real character $\chi$ on ratio orbits with $\chi(1)=1$ and $\chi(xy)=\chi(x)\chi(y)$ whenever the rational representatives are nonzero, such that for every orbit $q$ with positive rational representative, $(F q)$ equals $(\chi(q)+\chi(q)^{-1})/2-1$ as a real, and for each integer $n$ with $2\le n\le 5$ the sum $\chi(n)+\chi(n)^{-1}$ is rational.
background
In Recognition Science the native cost on positive ratios is forced to the unique J-cost $J(x)=(x+x^{-1})/2-1$ (T5). Here costs act on ratio orbits: equivalence classes of positive rationals under the ledger's identification. A real ratio character $\chi$ is a multiplicative map $\mathrm{RatioOrbit}\to\mathbb{R}$ with $\chi(1)=1$; the associated cost is $\mathrm{costFromRealCharacter},\chi,q=(\chi q+(\chi q)^{-1})/2-1$.
The structural pack PRCStructuralNativeCostHypothesesSansAnchor collects the ledger axioms without an absolute anchor: base-sans-two reciprocity, sign-reversing, monotonicity, and zero-calibrated doubled trace. The lighter pack SansAnchorHypotheses is what the factorization engine consumes. Upstream, realCharacterFactorizationHypotheses_of_structural shows the structural fields imply that light pack fieldwise. The heavy lifting lives in SansAnchorRealCharacterFactorizationTarget_proved: every such $F$ admits a principal real character whose J-cost recovers $F$ on positive orbits, with rational small traces on $n=2..5$.
proof idea
One-line term proof. Apply SansAnchorRealCharacterFactorizationTarget_proved to $F$, feeding it the light hypothesis pack produced by realCharacterFactorizationHypotheses_of_structural hF. That upstream theorem already returns the witness character (the real-character candidate), the character axioms, pointwise cost agreement, and rationality of the $n\in{2,3,4,5}$ traces. No extra algebra is done at this site.
why it matters
This is the bridge from the structural native-cost ledger to the real-character factorization used by gauge-orbit classification. Downstream, GaugeOrbitIsSignedPowerFamily asserts that every anchor-free structural inhabitant is either the zero-exponent sign cost or a sign-extended power cost of some nonnegative integer exponent; that classification rests on having the real factorization in hand for every structural $F$.
Framework-wise it instantiates T5 (J-uniqueness) on the orbit category without an absolute anchor, and feeds the RCL-compatible display $(\chi+\chi^{-1})/2-1$. The small-trace rationality side-condition is the hook later used by six-exponentials input when pinning exponents. Closing this structural-to-character arrow is what lets the signed-power family theorem quantify over the full structural class rather than an ad-hoc subclass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.