twoAdicGeneratedNativeCost_hypotheses
plain-language theorem explainer
The two-adic axis-twist generated cost satisfies the three native cost axioms: reciprocal symmetry, normalization invariance, and the canonical Recognition Composition Law, all up to ratio-orbit cross-equality. Anyone building alternative native costs or attacking uniqueness cites this certificate. The proof transfers each axiom from the character-built cost across the generating crossEq bridge, then reassembles RCL by add/mul congruence.
Claim. The two-adic generated native cost $C_{2}$ obeys the native cost package: $C_{2}(q^{-1})\sim C_{2}(q)$, $C_{2}(\mathrm{normalize}\,q)\sim C_{2}(q)$, and the canonical RCL $$C_{2}(xy)+C_{2}(x/y)\sim 2C_{2}(x)C_{2}(y)+2C_{2}(x)+2C_{2}(y)$$ for admissible positive ratio orbits $x,y$, where $\sim$ is cross-multiplication equality of ratio orbits.
background
In the Primitive Recognition Calculus, costs take values in ratio orbits (pairs of signed $\delta$-orbits for numerator and denominator). Equality is internal: crossEq is cross-multiplication balance of scaled numerators and denominators, equivalent to ordinary rational equality of the verifier displays.
A native cost package asks three structural laws on such a cost: reciprocal symmetry under $q\mapsto q^{-1}$, invariance under ratio normalization, and the canonical Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ written in orbit arithmetic. The two-adic axis-twist character is a ratio character; costFromCharacter builds a cost from it that already satisfies those laws. The two-adic generated native cost is the orbit-level object tied to that character cost by a generating crossEq bridge.
Upstream, reciprocal is the ratio-inversion automorphism on events and on the $J$-automorphism group; RCL is the same functional equation that forces $J(x)=\cosh(\log x)-1$ in the T5 uniqueness chain once analytic hypotheses are restored.
proof idea
Three structure fields, each by transferring known character-cost laws across the generating bridge.
Reciprocal: chain crossEq_trans of (generated $\sim$ character cost at $q$), then costFromCharacter_reciprocal_congr for the two-adic axis-twist character, then the symmetric bridge at $\mathrm{recip},q$.
Normalized invariant: same pattern with costFromCharacter_normalized_congr and the bridge at the normalized ratio.
Canonical RCL: instantiate RCL for the character cost via costFromCharacter_canonical_rcl. Congruence lemmas (ratioOrbit_add_congr, ratioOrbit_mul_congr) move each summand and product from character values to generated values (using the bridge and its symmetric), then reassemble the right-hand side. Reflexivity of crossEq handles the constant factor two.
why it matters
This is the native-hypotheses certificate for the two-adic twist cost. Downstream it is packaged into the sans-pair slim class (twoAdicGeneratedNativeCost_sans_pair_hypotheses) and into the constructed target PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget_constructed.
It also feeds PRCNativeCostUniquenessTarget_refuted: once a second native cost (the two-adic generated one) is known to satisfy the package and disagrees with the classical cost on a composite direction, bare uniqueness of native costs fails. In framework terms this separates the algebraic native package (reciprocal, normalize, RCL) from the analytic forcing that pins $J$ in T5; RCL alone on ratio orbits does not force a unique native cost without further regularity or minimality hypotheses.
The certificate is therefore a positive construction used both to inhabit alternative cost classes and to delimit what uniqueness can mean in PRC.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.