PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
Defines the signed-repaired factorization target for native cost fields: every F obeying the signed strengthened native-cost hypotheses must factor, up to cross-multiplication equality of ratio orbits, through some signed-admissible rational character. Uniqueness and minimality arguments cite this Prop as the intermediate claim that would force character-generated costs. The body is a pure universal-existential interface, not a proved theorem.
Claim. For every map $F$ from ratio orbits to ratio orbits that satisfies the signed strengthened native-cost hypotheses (strengthened native-cost axioms plus signed-unit calibration), there exists a map $\chi$ that is a signed-admissible ratio character (admissible character plus signed-unit calibration) 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, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are related by cross-equality when the scaled numerators balance as signed orbits (the internal PRC stand-in for rational equality).
A cost field is a self-map $F$ on ratio orbits. The cost generated from a character $\chi$ is the orbit map obtained by applying the on-ratio-orbit construction to $\chi(q)$. Signed-admissible characters strengthen ordinary admissibility by requiring explicit preservation of the signed unit; the signed strengthened native-cost hypotheses likewise add signed-unit calibration to the pass-274 strengthened native-cost package.
This module packages uniqueness and factorization targets after the absolute-value no-go. The present definition is the pass-281 repaired factorization target: under the native signed-unit cost field, any factor must itself be signed-admissible.
proof idea
Definitional Prop, not a proved statement. The body is a single quantified interface: universal over cost fields $F$ carrying signed strengthened native-cost hypotheses, existential over characters $\chi$ that are signed-admissible, with pointwise cross-equality between $F(q)$ and the character-generated cost at every ratio orbit $q$. No tactics or lemmas are applied; downstream theorems either inhabit or refute this Prop.
why it matters
This target is the signed-repaired bridge between native-cost hypotheses and character factorization after pass 281. Downstream, it feeds the uniqueness target: if every such $F$ factors through a signed-admissible character, then uniqueness of the native cost follows by transporting cross-equality. A companion lemma derives the target from ordinary character factorization plus two-calibration forcing prime calibration.
It is also the object of a minimality corollary that refutes it: the signed-strengthened ledger cannot factor every inhabitant through a signed-admissible character, because the zero-flat cost cannot factor (character-generated costs are canonical at the zero orbit). That refutation closes a scaffolding path in the native-cost uniqueness program and sharpens why signed-unit calibration alone does not yield a unique character factorization for every admissible field.
In the broader Recognition forcing chain this sits inside the foundation layer that isolates the J-cost and its uniqueness (T5), before phi and the eight-tick structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.