PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted
plain-language theorem explainer
The signed-strengthened native-cost ledger cannot factor every admissible cost through a signed-admissible character. Anyone tracking uniqueness or selection of the RS native cost on the signed-strengthened class would cite this negative result. The proof is a one-line composition: factorization would imply uniqueness, and uniqueness is already refuted by the zero-flat countermodel.
Claim. It is not the case that every inhabitant of the signed-strengthened native-cost class factors through a signed-admissible character. Equivalently, the signed-admissible character-factorization target for that class is false.
background
In the Primitive Recognition Calculus, native costs are real-valued functionals on ratio orbits (ledger displays of multiplicative structure). The signed-strengthened class strengthens the base ledger by pairs and a signed unit, still without a zero field: every field lives on nonzero orbits.
A signed-admissible character is a character-shaped generator meant to produce costs that are canonical on the zero orbit. The factorization target asserts that every cost in the signed-strengthened class arises this way. The uniqueness target asserts a unique native cost on that class.
Upstream, uniqueness is already refuted: "the signed-strengthened ledger (base + pairs + signed unit, no zero field) admits the zero-flat countermodel." Character-generated costs are canonical at the zero orbit, so the zero-flat cost cannot arise from such a factorization.
proof idea
Term-mode one-liner. Assume a proof $h$ of the signed-admissible character-factorization target. Apply the transport lemma that turns any such factorization into a proof of the uniqueness target. Feed that into the already-proved uniqueness refutation (zero-flat countermodel on the signed-strengthened hypotheses). Contradiction, so the factorization target is false.
why it matters
This closes a named corollary in the native-cost minimality module: factorization through signed-admissible characters cannot rescue uniqueness on the signed-strengthened ledger. It sits beside the uniqueness refutation and clears the path toward zero-calibrated or slim-class uniqueness statements (siblings such as the zero-calibrated uniqueness target and slim-class equivalences).
In the broader RS foundation, native-cost selection feeds the J-cost story (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Showing that character factorization fails on the signed-strengthened class forces the calculus either to add zero-orbit calibration or to shrink the hypothesis class before claiming a unique native cost. No downstream consumers are wired yet; the result is a negative gate on over-strong uniqueness claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.