PRCPrimeSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
Defines the final repaired factorization target: any native cost F that already carries prime and signed-unit calibration factors through a signed-admissible ratio character χ, with F(q) cross-equivalent to the character-generated cost at every ratio orbit q. Cited by the bridge from ordinary character factorization into uniqueness. Pure Prop packaging; no proof content.
Claim. For every map $F$ on ratio orbits satisfying the prime-signed strengthened native-cost hypotheses, there exists a signed-admissible ratio character $\chi$ such that for all ratio orbits $q$, $F(q)$ is cross-multiplication equivalent to the cost generated from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, costs and characters act on ratio orbits: pairs of a signed integer orbit numerator over a nonzero distinction-nat denominator. Two ratio orbits are identified by cross-equivalence when scaled numerators balance under the internal signed-orbit relation (K4.10), the PRC stand-in for rational equality.
A cost generated from a character $\chi$ is the orbit map $q \mapsto \mathrm{onRatioOrbit}(\chi(q))$; the canonical native cost is the identity-character case. The prime-signed strengthened native-cost hypotheses package signed strengthened structure plus direct all-prime calibration at the cost level. A signed-admissible ratio character is an admissible character that also preserves the signed unit (the unsigned interface alone cannot force that field).
This module packages uniqueness and factorization targets for native costs under successively stronger calibration interfaces. The present definition is the factorization target at the prime-signed strengthened layer.
proof idea
Definitional Prop abbreviation only: the body is the universal-existential statement above, with no tactics or lemmas. Downstream theorems discharge or consume it by unpacking the structure fields and applying ordinary character factorization plus cross-equivalence transitivity.
why it matters
Closes the repaired factorization interface at the prime-signed strengthened layer: once the native cost itself is prime-calibrated and signed-unit calibrated, ordinary character factorization is enough to produce a signed-admissible factor. Downstream, ...Target_of_character_factorization lifts the weaker native-cost character-factorization target into this one, and ...UniquenessTarget_of_signed_admissible_factorization turns the factorization into the uniqueness target by cross-equivalence transitivity against the identity-character cost.
In the Recognition framework this sits inside the foundation forcing path toward J-uniqueness (T5) and the Recognition Composition Law: native cost must be forced as the unique admissible character cost on the ratio-orbit display before continuum J-cost and the phi fixed point are recovered. It is interface glue, not a physics theorem, but it is the precise Prop that uniqueness proofs at this calibration strength invoke.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.