canonicalSelectedNativeCost_full_hypotheses
plain-language theorem explainer
The canonical selected native cost inhabits the full zero-calibrated, prime-signed, strengthened native-cost hypothesis class, so the frozen PRC cost-selection ledger is non-vacuous. Anyone citing native J-uniqueness or the cost-selection package needs this witness. The proof packs prior native and cross-equation lemmas into the structure and discharges zero-calibration by rational reduction and norm_num.
Claim. The canonically selected native cost functional satisfies the full PRC hypothesis package: it is a zero-calibrated, prime-signed, strengthened native cost. In particular its doubled-trace calibration vanishes at the identity orbit, signed unit and prime-direction costs match the cross-equation on the corresponding ratio orbits, and the underlying native strengthened axioms hold.
background
Primitive Recognition Calculus (PRC) isolates the native cost that Recognition Science uses on ratio orbits before the classical J-cost is recovered. A native cost is a real-valued functional on ratio-orbit data; the strengthened native package adds reciprocity-style and product constraints along prime directions. Prime-signed structure further requires matching costs on the negative unit orbit and on each prime direction; zero-calibration requires the doubled-trace combination to vanish at the identity (the two-calibration field of the frozen ledger).
The local module selects one canonical witness and proves it meets every layer of that ledger. Upstream, canonicalSelectedNativeCost_native_hypotheses already places the witness in the native strengthened class, and canonicalSelectedNativeCost_crossEq_onRatioOrbit identifies its values with the cross-equation on ratio orbits (via the rational presentation toRat). Cost language elsewhere in the monolith (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen summed weights) is the ambient meaning of "cost"; here the object is still the native PRC functional, not yet the classical $J(x)=(x+x^{-1})/2-1$.
The doc-comment states the point bluntly: the selected witness makes the frozen ledger non-vacuous.
proof idea
Tactic proof that builds the nested hypothesis structure field-by-field.
For the prime-signed block: native strengthened data is exactly canonicalSelectedNativeCost_native_hypotheses; prime-pair product cost and signed-unit cost are instances of canonicalSelectedNativeCost_crossEq_onRatioOrbit on the product of two prime directions and on the negative-one ratio orbit; prime-direction cost is the same lemma on a single prime direction.
Zero-calibration rewrites the doubled-trace predicate into a rational cross-equation (RatioOrbit.crossEq_iff_toRat_eq), unfolds doubled-trace and the selected cost's toRat formula on the relevant orbit operations (mul, add, two, one, zero), then finishes by norm_num.
why it matters
This is the non-vacuity half of native cost selection. Downstream, costSelectionPackageNative_holds packages J-uniqueness with an explicit witness pair (canonicalSelectedNativeCost, canonicalSelectedNativeCost_full_hypotheses) plus the cross-equation lemma, so the native selection package is inhabited rather than a pure uniqueness statement. The slim-class theorem canonicalSelectedNativeCost_slim_hypotheses is the one-line transport of this result across the slim/full equivalence. The premise-ledger theorem records that every deposited obligation sits at the $\delta$-only strength tag.
In the forcing chain this sits under T5 (J-uniqueness): the classical cost $J(x)=\cosh(\log x)-1$ is forced only after a native selection and calibration story is non-empty. The module's frozen decoys (constant-zero and linear costs) are required to fail the same class, so this theorem is the positive counterpart that keeps the ledger from being empty while those smoke tests stay excluded.
It does not itself prove uniqueness; uniqueness is the companion target consumed by the same package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.