PRCNativeCostHypotheses
plain-language theorem explainer
Packages the five discrete axioms a cost map on ratio orbits must obey to count as a PRC-native cost: reciprocity, normalization invariance, the Recognition Composition Law, unit-zero, and two-calibration. Downstream uniqueness, selection, and minimality ledgers cite this structure as the base premise pack. It is a Prop-valued structure, not a proved theorem.
Claim. A map $F$ from ratio orbits to ratio orbits is a PRC-native cost candidate when: (i) $F(q)$ and $F(q^{-1})$ are cross-equal for every orbit $q$; (ii) $F$ is invariant under ratio normalization; (iii) on nonzero orbits, $F(xy)+F(x/y)$ is cross-equal to $2F(x)F(y)+2F(x)+2F(y)$ (canonical RCL); (iv) $F(1)=0$; (v) $F(2)$ is cross-equal to the canonical discrete $J$-cost of the two-orbit.
background
Primitive Recognition Calculus works on ratio orbits: discrete equivalence classes of positive rational recognition ratios, with cross-equality as the native equality predicate and operations (mul, recip, add, normalize) lifted from the rational surface. The sibling onRatioOrbit embeds the continuous $J$-cost $J(x)=(x+x^{-1})/2-1$ onto that discrete surface.
The Recognition Composition Law (RCL) is the functional equation forced upstream in the T5 $J$-uniqueness step: $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Here it is restated purely in ratio-orbit arithmetic as canonical_rcl, so classification can stay on the discrete ledger before any real completion.
Module context is the PRC $J$-cost layer: native hypotheses first, continuous positive-real uniqueness only as a later corollary. The two_calibrated field is the discrete stand-in for unit log-curvature calibration; without it the zero map would satisfy the other four axioms.
proof idea
No proof body: this is a Prop-valued structure definition. Each field is a named hypothesis on a map $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$. Downstream proofs either construct an instance field-by-field (as for the canonical selected native cost) or assume an instance and project fields (e.g. only canonical_rcl into the doubled-trace d'Alembert identity).
why it matters
This is the base premise ledger for the entire PRC-native cost program. PRCNativeCostUniquenessTarget quantifies over exactly these hypotheses and asks that every such $F$ agree with onRatioOrbit. Selection theorems prove the canonical witness satisfies the pack and that constant-zero and linear competitors fail it (zero fails two-calibration). Slim minimality certificates embed it as the native field, and doubledTrace_dAlembert_of_native specializes the real character factorization to maps obeying only the RCL field of this pack.
In the forcing chain this is the discrete surface form of T5 $J$-uniqueness plus RCL, held on ratio orbits so the continuous theorem becomes a corollary rather than a premise. The open target remains full native classification on normalized orbits before real transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.