PRCZeroCalibratedNativeCostCharacterFactorizationTarget
plain-language theorem explainer
Any native cost F on ratio orbits that obeys the PRC cost hypotheses and has zero-calibrated doubled d'Alembert trace factors as the cost generated by some ratio character χ, up to cross-multiplication equivalence. Cost-uniqueness and foundation-ledger authors cite this repaired factorization interface. The declaration is a pure Prop target; a sibling theorem discharges it by lifting the doubled trace to a character and matching costs.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the native cost hypotheses (reciprocal symmetry, normalization invariance, and the canonical recognition composition law) and the doubled trace $T_F(q)=2(F(q)+1)$ is cross-equivalent to zero at the zero orbit, then there exists a ratio character $\chi$ such that for every ratio orbit $q$, $F(q)$ is cross-multiplication equivalent to the cost generated from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Equality of displays is internal cross-multiplication equivalence (balanced scaled numerators), not external real equality. A native cost is a self-map F of ratio orbits obeying reciprocal symmetry, invariance under normalization, and the canonical recognition composition law on the discrete rational surface.
The doubled d'Alembert trace of such an F is $T_F(q)=2(F(q)+1)$. For costs generated from a character this recovers $\chi(q)+\chi(q)^{-1}$. Zero-calibration requires $T_F(0)\sim 0$; without it the nonzero d'Alembert law cannot pin the zero orbit. Cost from a character is the orbit map obtained by applying the on-ratio-orbit construction to $\chi(q)$.
This module packages uniqueness of native costs as exact Lean targets. The present definition is the zero-calibrated character-factorization target: every admissible zero-calibrated F must arise from some ratio character up to crossEq.
proof idea
Definitional Prop, not a proved theorem. The body is a single quantified implication: native cost hypotheses on F plus zero-calibration of nativeCostDoubledTrace F yield existence of a ratio character χ with F crossEq-equal to costFromCharacter χ pointwise. No tactics or lemmas are invoked at the definition site; discharge lives in the sibling theorem that proves the target by lifting the doubled trace to a character and matching costs.
why it matters
This is the repaired factorization half of zero-calibrated native cost uniqueness, sitting on the path toward the J-cost uniqueness landmark (T5: $J(x)=(x+x^{-1})/2-1$) inside the PRC discrete surface. Downstream, the uniqueness-of-character-targets lemma consumes it together with character rigidity to obtain the full zero-calibrated uniqueness target. The blocker certificate records it as an exact open-math split, and the universal foundation ledger lists it among positive repaired interfaces (while uniqueness itself is recorded as refuted on the old route).
A sibling theorem already proves the target holds, and another records that the older non-zero-calibrated factorization target is refuted. The net effect is to isolate zero-calibration as the necessary repair: factorization through characters works once the doubled trace is forced to vanish at zero, aligning discrete native costs with the continuous RCL/J picture without smuggling an external real completion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.