prcTwoThreeCompositeLocalForkCertificate
plain-language theorem explainer
Packages a closed certificate for the exact 2×3 two-adic fork: pairwise equivalences among local-orientation failure, ratio-axis twist, and prime-calibrated two-adic twist, plus the positive local-orientation target as the negation of each witness. Downstream universal-foundation wiring cites it so the equivalence chain need not be rebuilt. Construction is field-by-field application of prior iff and absurd lemmas, with three short compositions for cost-consistency exclusions.
Claim. There is a closed certificate for the exact $2\cdot 3$ two-adic fork asserting: local-orientation failure $\leftrightarrow$ two-adic axis-twist ratio character $\leftrightarrow$ prime-calibrated two-adic axis-twist character; the local-orientation target is equivalent to the negation of each of those three; the target excludes the calibrated twist; absence of failure forces the target; and each of mixed-composite cost consistency, prime-identity-forces-two, and prime-pair product cost consistency excludes the failure character.
background
In the Primitive Recognition Calculus native-cost uniqueness development, candidate cost characters on the multiplicative group are constrained by d'Alembert-type functional equations and by calibration at primes. A two-adic axis-twist ratio character is a ratio character that twists along the 2-adic axis; a prime-calibrated two-adic axis-twist character is the same object under the prime-calibration packaging. Local-orientation failure for the $2\cdot 3$ composite is the constructive witness that orientation at that composite fails, while the local-orientation target is the positive statement that orientation holds.
The structure being inhabited packages, under one name, the full equivalence chain among failure, ratio twist, and calibrated twist, together with the positive branch (target as negation of each equivalent witness). Upstream lemmas already prove each link: calibrated twist iff ratio twist; failure iff calibrated twist; target iff no ratio twist / no failure / no calibrated twist; and three absurdities that mixed-composite cost consistency, prime-identity-forces-two, and prime-pair product cost consistency each kill the ratio-twist character (hence the failure character after transport).
proof idea
Definitional inhabitant of the certificate structure. Six fields are one-line wrappers naming the corresponding prior iff theorems (failure iff ratio twist; calibrated iff ratio twist; failure iff calibrated; target iff no ratio / no failure / no calibrated). The exclusion target_excludes_calibrated_two_adic_axis_twist is the prior absurdity of calibrated twist under the orientation target. no_failure_character_forces_target is the prior implication from no-failure to target.
The three cost-consistency exclusions are short tactic blocks: assume the consistency hypothesis and a failure character; transport failure to a ratio-twist character via PRCTwoAdicAxisTwistRatioCharacter_of_two_three_local_orientation_failure_character; then apply the matching absurdity (absurd_of_mixed_composite_cost_consistency, absurd_of_prime_identity_forces_two, or absurd_of_prime_pair_product_cost_consistency).
why it matters
Gives a single named handle for the exact $2\cdot 3$ two-adic fork so downstream certificate wiring does not repeat the equivalence chain. The sole recorded consumer is prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into the conditional universal-foundation package.
In the Recognition forcing picture this sits inside native-cost uniqueness for the Primitive Recognition Calculus: ruling out (or packaging the ruling-out of) two-adic axis twists at the first mixed composite $2\cdot 3$ is part of forcing the unique J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\varphi$ (T6). It does not itself close T5–T8; it is scaffolding glue for the universal-foundation conditional certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.