PRCZeroCalibratedPrimeSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget
plain-language theorem explainer
Defines the final factorization target for zero-calibrated native cost: any F meeting the zero-calibrated prime-signed strengthened hypotheses factors, up to cross-equivalence of ratio orbits, through a signed-admissible character. Cited by the uniqueness blocker certificate and by the theorem that discharges this target. The body is a pure Prop packaging of that universal-existential statement.
Claim. For every map $F$ on ratio orbits that satisfies the zero-calibrated prime-signed strengthened native-cost hypotheses, there exists a signed-admissible ratio character $\chi$ such that for every ratio orbit $q$, $F(q)$ is cross-equivalent to the cost generated from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, costs and characters act on ratio orbits: each orbit is a signed-integer numerator over a nonzero distinction-nat denominator. Two orbits are identified by cross-equivalence when the scaled numerators balance as signed orbits (the internal PRC stand-in for rational equality).
A cost generated from a character $\chi$ is the orbit map $q \mapsto$ the on-ratio-orbit image of $\chi(q)$; the canonical native cost is the identity-character case. Signed-admissible characters strengthen ordinary admissibility by preserving the signed unit (the unsigned interface alone cannot force that field).
The hypothesis package on $F$ combines prime and prime-pair signed strengthened native-cost axioms with zero calibration of the doubled trace of $F$ at the zero orbit. The local module goal is native-cost uniqueness via character factorization along this repaired route.
proof idea
No proof: this is a def equating a name to a Prop. The right-hand side is the quantified statement itself (universal over $F$, implication from the zero-calibrated prime-signed strengthened hypotheses, existential over a signed-admissible character matching $F$ pointwise under cross-equivalence via costFromCharacter). Discharge is deferred to the sibling theorem that proves the target by reducing to the unsigned zero-calibrated factorization result and repairing the signed-unit field.
why it matters
This is the repaired end-state for the character-factorization route to native-cost uniqueness: zero calibration plus prime-signed strengthening should force a signed-admissible factor, not merely an unsigned admissible one. Downstream, the blocker certificate records that native-cost uniqueness is not fully closed and splits the gap into exact Lean targets; this definition is the signed-admissible zero-calibrated factorization slot in that ledger. The companion _proved theorem asserts the target holds, feeding the uniqueness program that pins the PRC cost to the J-cost shape forced at T5 in the unified forcing chain (and thereby the Recognition Composition Law). It does not by itself finish uniqueness; it names the precise Prop the route must hit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.