SansAnchorRealCharacterFactorizationTarget
plain-language theorem explainer
Packages the corrected factorization target: every anchor-free ledger map F factors through a real multiplicative character χ whose J-cost display recovers F on positive orbits, with rational doubled traces at bases 2..5. Anyone closing native-cost uniqueness or the exponent step cites this Prop. It is pure definitional packaging; the companion theorem discharges it.
Claim. For every map $F$ from ratio orbits to ratio orbits satisfying the anchor-free native-cost hypotheses (base-sans-two, sign-reversing, monotone, and zero-calibrated doubled trace), there exists a real-valued character $\chi$ on ratio orbits that is unital ($\chi(1)=1$) and multiplicative, such that for every positive orbit $q$ one has $F(q)=(\chi(q)+\chi(q)^{-1})/2-1$ as reals, and for each integer base $n\in\{2,3,4,5\}$ the doubled trace $\chi(n)+\chi(n)^{-1}$ is rational.
background
Ratio orbits are the PRC display of rational numbers: a signed integer numerator over a nonzero distinction-nat denominator, with toRat the verifier transport to $\mathbb{Q}$. The native cost ledger is a map $F$ on those orbits. Anchor-free hypotheses package four structural axioms on $F$: a base condition excluding the two-case, sign-reversal, monotonicity, and zero-calibration of the doubled trace built from $F$.
A real ratio character $\chi$ is a unital multiplicative map $\mathrm{RatioOrbit}\to\mathbb{R}$. The cost reconstructed from such a character is the classical $J$-form
$$\mathrm{costFromRealCharacter}(\chi,q)=\frac{\chi(q)+\chi(q)^{-1}}{2}-1,$$
exactly the T5 unique cost functional $J(x)=(x+x^{-1})/2-1$. Small natural bases embed as orbits via natOrbit.
This module sits in the Cost domain and imports the real-trace root, rational-exponent, and PRC native-cost uniqueness layers. The target is the corrected (anchor-free) factorization statement that those layers need before the exponent step can fire.
proof idea
Definitional Prop only: no tactic or term proof. The body is the universal quantification over ledger maps $F$, the implication from the four-field anchor-free hypothesis pack, and the existential claim of a real character $\chi$ with three conjuncts (character axioms, pointwise cost agreement on positive orbits, rational doubled traces at $n=2..5$). Discharge lives in the companion theorem, which builds an explicit candidate character and checks the three conjuncts.
why it matters
This is the corrected factorization target for the anchor-free native-cost ledger. Downstream, the input abbrev is literally this Prop, and SansAnchorRealCharacterFactorizationTarget_proved asserts it, constructing a real principal character whose cost display matches $F$ and whose small-base traces are rational so the rational-exponent step can fire.
In the Recognition framework the cost display is forced to be $J$ (T5 J-uniqueness; RCL). Factoring every structural ledger through a real multiplicative character is the bridge from the discrete PRC ledger to the continuous $J$-cost used in mass ladders and coupling constants. Without rational traces at bases $2..5$, the exponent identification that feeds the phi-ladder does not start. The declaration therefore sits on the Cost path that underwrites uniqueness of native cost and the later constant extractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.