absValueGeneratedNativeCost_native_hypotheses
plain-language theorem explainer
The absolute-value-generated native cost on ratio orbits satisfies the three native cost axioms: reciprocity, normalization invariance, and the canonical Recognition Composition Law. Anyone working on PRC cost uniqueness or zero-calibration refutations cites this as the witness that a concrete cost meets the native package. The proof transfers each axiom from the character-built cost across cross-multiplication equivalence of orbits.
Claim. The native cost built from the absolute-value character on ratio orbits satisfies the native cost hypotheses: (i) cost of a ratio equals cost of its reciprocal (up to cross-multiplication equivalence of orbits); (ii) cost is invariant under ratio normalization; (iii) for positive ratios $x,y$, the Recognition Composition Law holds: $\mathrm{cost}(xy)+\mathrm{cost}(x/y)$ is cross-equivalent to $2\,\mathrm{cost}(x)\,\mathrm{cost}(y)+2\,\mathrm{cost}(x)+2\,\mathrm{cost}(y)$.
background
In the Primitive Recognition Calculus, costs live on ratio orbits (pairs of signed $\delta$-orbits for numerator and denominator). Equality of costs is not pointwise identity but crossEq: two orbits match when cross-multiplication balances as signed orbits (the internal PRC rational relation, choice-free).
A native cost is a map from ratio orbits to ratio orbits obeying three structural axioms: reciprocity under inversion of the ratio, invariance under the distinction-normalization of the ratio, and the canonical Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. The absolute-value character induces a cost via costFromCharacter; the absolute-value-generated native cost is the concrete generator that is cross-equivalent to that character cost on every orbit.
Upstream, crossEq is reflexive, symmetric, and transitive, and the character cost already satisfies reciprocity, normalization congruence, and canonical RCL. The present theorem packages those facts into the native-hypothesis structure for the generated cost.
proof idea
Three structure fields, each by transferring across crossEq.
Reciprocal: for orbit $q$, chain absValueGeneratedNativeCost_crossEq_generated q to the character-cost reciprocal congruence for the absolute-value character, then back via symmetry of the generator equivalence at recip q.
Normalized invariant: same pattern with costFromCharacter_normalized_congr and the generator equivalence at the normalized ratio.
Canonical RCL: let $C$ be the character cost. Invoke costFromCharacter_canonical_rcl for $C$. Congruence lemmas for orbit addition and multiplication (ratioOrbit_add_congr, ratioOrbit_mul_congr) move both sides of the RCL identity from $C$ to the generated cost, using generator cross-equivalence at $x$, $y$, $xy$, and $x/y$, plus reflexivity on the constant two. Transitivity of crossEq closes the identity.
why it matters
This is the native-hypothesis witness for the absolute-value-generated cost inside PRC native-cost uniqueness. Downstream it is the native field of the strengthened package (absValueGeneratedNativeCost_strengthened_hypotheses), and it is the concrete cost fed into three refutation theorems: uniqueness of zero-calibrated native cost is refuted; signed admissible character factorization under zero calibration is refuted; and zero calibration forcing signed-unit calibration is refuted.
In the Recognition framework this sits under the cost-uniqueness side of the forcing story that isolates the J-cost (T5: $J(x)=(x+x^{-1})/2-1$) and the RCL as the composition law. By exhibiting a native cost that meets the axioms yet fails stronger zero-calibration or signed-unit demands, the module rules out over-strong uniqueness targets and keeps the admissible cost class aligned with the character-trace route rather than an absolute-value shortcut.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.