PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget
plain-language theorem explainer
Names the universal consistency target that prime-calibrated ratio characters must still match native cost on every mixed composite direction 2·p. Under the orientation that sends the 2-axis to its reciprocal and a distinct native prime p to the identity, the character-derived cost on 2·p is forced equal (by cross-multiplication) to the native on-orbit cost. Downstream uniqueness and absurdity lemmas cite this Prop as the cost-visible branch-rigidity blocker. The body is a pure Prop abbreviation, not a proved statement.
Claim. For every map $\chi$ on ratio orbits that is a PRC ratio character, is prime-direction calibrated, and satisfies $\chi(2)\sim 2^{-1}$ under cross-multiplication, the following holds: whenever $p$ is a native prime orbit distinct from $2$ with $\chi(p)\sim p$, the character-derived cost of the composite direction $2\cdot p$ is cross-equivalent to the native cost of $2\cdot p$ on ratio orbits.
background
In the Primitive Recognition Calculus, ratio orbits are rational displays built from signed integer orbits over nonzero distinction-nat denominators. Two ratio orbits are identified by crossEq when cross-multiplication of numerator and denominator balances as signed orbits (the internal PRC stand-in for rational equality). Reciprocals and products of ratio orbits are total operations on this display.
A PRC ratio character $\chi$ is a structure-preserving map on ratio orbits. Prime-direction calibration means $\chi$ acts in a controlled way on native prime directions (orbits that are nonzero, non-unit, and free of nontrivial factorization). The native cost on ratio orbits is the J-cost pulled back along the orbit display; a parallel cost can be rebuilt from the character itself.
The local module studies uniqueness of that native cost under prime calibration. The mixed-orientation surface singled out here sends the 2-direction to its reciprocal while fixing a distinct prime $p$ at the identity. The product $2\cdot p$ is the first composite where orientation mismatch can produce a cost defect.
proof idea
There is no proof obligation: the declaration is a def equating a name to an explicit universal Prop. The body quantifies over characters $\chi$, packages the standing hypotheses (ratio character, prime-direction calibration, reciprocal action on the 2-direction), then for each native prime $p\neq 2$ fixed at identity by $\chi$, asserts cross-equivalence of the character-derived cost and the native on-orbit cost on the product direction $2\cdot p$. Downstream theorems treat the name as a hypothesis or as one side of an iff chain.
why it matters
This target is the cost-visible form of the current branch-rigidity blocker in native-cost uniqueness: prime calibration must propagate through the mixed composite $2\cdot p$. Downstream, assuming the target immediately kills the two-adic axis-twist character and the reciprocal-identity non-two composite cost-defect character. It is also proved equivalent to several sibling targets (prime-identity forces two-prime identity; prime-pair product cost consistency; absence of non-two mixed characters; absence of composite cost-defect characters).
In the broader Recognition forcing chain, native J-cost uniqueness (T5: $J(x)=(x+x^{-1})/2-1$) is the algebraic backbone of the Recognition Composition Law. Closing the mixed $2\cdot p$ surface is the remaining local obstruction before prime calibration forces the global native cost, so the framework can lock the self-similar fixed point $\phi$ and the eight-tick octave without residual character defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.