PRCTwoThreeCompositeLocalForkCertificate
plain-language theorem explainer
Closed Prop certificate for the exact 2×3 two-adic fork: the constructive failure witness, the uncalibrated ratio-character axis twist, and the prime-calibrated twist are packaged as equivalent, and the positive local-orientation target is exactly the negation of each. Downstream certificate wiring cites this bundle instead of replaying the equivalence chain. Definitional packaging of already-named branch interfaces; the filled instance lives one declaration below.
Claim. A closed certificate asserting mutual equivalence of three constructive witnesses: existence of a ratio character with two-adic axis twist that fails local orientation at the composite $2\cdot 3$; existence of any ratio character with two-adic axis twist; and existence of a prime-calibrated ratio character with that same twist. The positive target (every ratio character carrying the two-adic axis twist is locally oriented at $2\cdot 3$) is equivalent to the negation of each witness, is implied by absence of the failure witness, and is forced whenever any of the mixed-composite, one-sided prime-identity, or prime-pair product cost-consistency targets hold.
background
In the primitive recognition calculus, ratio characters are maps on ratio orbits that preserve the multiplicative cross-equation structure used to read native cost. A two-adic axis twist is the branch behavior that sends the orbit-$2$ prime direction to its reciprocal. Local orientation at the first mixed composite $2\cdot 3$ asks that any such twisted character still choose one of the two canonical orientations on that composite direction.
The failure character is the existential countermodel surface: some ratio character twists the two-adic axis and fails that local orientation. The uncalibrated twist target drops the orientation failure and keeps only the twist; the calibrated variant adds prime-direction calibration. Pass-level work already treats the uncalibrated twist as automatically carrying calibration once it is realized by a ratio character.
Cost-side blockers sit upstream as universal targets: prime calibration must force identity on orbit $2$ from identity on any calibrated prime, must propagate to prime-pair products, and must calibrate the mixed composite $2\cdot p$ even when orbit $2$ is reciprocal and a distinct native prime stays on identity. Those targets are the cost-visible routes that exclude the failure witness.
proof idea
No proof body: this is a structure of Prop fields, i.e. a named bundle of equivalences and one-way implications. Each field is a pure logical link among already-defined branch interfaces (failure character, uncalibrated twist, calibrated twist, positive local-orientation target, and the three prime-calibration cost-consistency targets). The concrete inhabitant prcTwoThreeCompositeLocalForkCertificate fills the fields by citing the corresponding _iff_ and exclusion lemmas; this declaration only fixes the certificate shape so downstream wiring names one object.
why it matters
Native cost uniqueness in PRC turns on whether two-adic branch behavior can escape character rigidity. This certificate collapses the $2\cdot 3$ fork to a single handle: constructive countermodel, uncalibrated twist, and calibrated twist are interchangeable, and the positive orientation target is their common negation. The filled instance prcTwoThreeCompositeLocalForkCertificate is the immediate consumer; PRCUniversalFoundationOpenTargets carries the broader ledger of repaired versus refuted foundation routes that this fork feeds. In the Recognition forcing chain the payload is J-uniqueness (T5) and the Recognition Composition Law read through ratio characters: if the positive branch holds, mixed composites cannot host a twisted two-adic countermodel, tightening the path to a unique native cost. Open question touched: whether the cost-consistency targets fully discharge the fork, or whether a residual calibrated twist still survives outside the $2\cdot 3$ local surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.