PRCNativeCostCharacterFactorizationTarget_refuted
plain-language theorem explainer
The unqualified claim that every admissible PRC-native RCL cost factors through a ratio character is false. Cite this when tracking the native-cost uniqueness blockers or the discrete d'Alembert factorization step. Proof is a one-line modus tollens: factorization would lift to a character-trace target already refuted.
Claim. It is false that every map $F$ on ratio orbits satisfying the PRC-native cost hypotheses admits a ratio character $\chi$ such that $F(q)$ is cross-equal to the cost induced by $\chi$ at every ratio orbit $q$.
background
In the Primitive Recognition Calculus, costs live on ratio orbits and are required to obey the Recognition Composition Law in native discrete form. A ratio character is a multiplicative map on those orbits; the cost built from a character is the discrete stand-in for classical J-cost factorization through d'Alembert solutions of the functional equation.
The proposition under attack says every $F$ meeting the PRC-native cost hypotheses factors that way: some character $\chi$ makes $F(q)$ cross-equal to the character cost at all $q$. The module doc labels this the first exact blocker and the discrete d'Alembert factorization step.
The same module already refutes the stronger character-trace lift target, and proves that any factorization witness produces such a lift. That implication is the only upstream fact this refutation needs.
proof idea
One-line reduction. Assume a factorization hypothesis. Feed it to the lemma that turns factorization into a character-trace lift witness. Apply the already-proved refutation of that lift target. Pure modus tollens; no new analytic work.
why it matters
Closes the unqualified factorization surface and forces the repaired interface: native hypotheses plus explicit zero calibration of the generated doubled trace (Pass 294). Downstream, the sharpened uniqueness refutation quotes this as its first conjunct; the zero-calibrated-not-old theorem packages the contrast with the proved calibrated target; and the uniqueness blocker certificate records the repaired surface as the live interface. In the RS chain this sits under T5 J-uniqueness and the RCL, showing discrete native uniqueness needs the zero-calibration side condition rather than bare factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.