SansAnchorRealCharacterFactorizationTarget_proved
plain-language theorem explainer
Every anchor-free ledger map on ratio orbits factors through a real principal character whose doubled traces at bases 2–5 are rational. Cost theorists cite this when reducing native-cost uniqueness to character extraction without fixing the value at two. The proof packages the candidate character and three already-proved properties into the existential target.
Claim. For every map $F$ on ratio orbits satisfying the anchor-free hypotheses, there exists a real-valued map $\chi$ that is a principal ratio character, agrees with the cost reconstructed from $\chi$ on every positive orbit, and has rational doubled traces $\chi(n)+\chi(n)^{-1}$ for integers $n$ with $2\le n\le 5$.
background
The module works in the Recognition cost layer: maps $F$ on ratio orbits that obey the Recognition Composition Law in doubled-trace form, without requiring a fixed anchor value at two. The doubled-trace d'Alembert identity is available from RCL alone (doubledTrace_dAlembert_of_rcl) and again under the full anchor-free package (doubledTrace_dAlembert_of_sansAnchor).
SansAnchorHypotheses packages those composition, positivity, and rationality constraints. From any such $F$ one extracts realCharacterCandidate, a real map that is either the sign character (degenerate doubled trace at two equal to 2) or a generalized linear extraction from the doubled trace. The cost reconstructed from a real character is costFromRealCharacter.
The target proposition demands three things of that candidate: it is a PRCRealRatioCharacter (unit, multiplicative, reciprocal), it reproduces $F$ on positive orbits, and its doubled traces at the small natural bases $2$ through $5$ are rational so later exponent steps can fire.
proof idea
One-line existential packaging. Introduce $F$ and the anchor-free hypotheses, then supply the witness realCharacterCandidate F together with the three supporting lemmas already proved for that candidate: it is a real ratio character, its reconstructed cost agrees with $F$ on positive orbits, and its doubled traces at $n\in{2,3,4,5}$ are rational. No further algebra is done at this site.
why it matters
Closes the corrected factorization target for anchor-free ledgers: every such $F$ factors through a real principal character with rational small traces. Downstream, structural_sansAnchor_realCharacterFactorization lifts the result to structural native-cost hypotheses, and the PRC structural ledger uses the factorization path when ruling out non-canonical cube-generated costs at two.
In the broader forcing picture this is the cost-side character step that feeds uniqueness of the native cost (toward T5 J-uniqueness and the RCL). Rational small traces are the bridge to the trace-rational-exponent machinery imported by the module, so the factorization is not merely existential: it is shaped for the exponent and gauge-orbit arguments that follow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.