zeroFlatNativeCost_hypotheses
plain-language theorem explainer
The zero-flat native cost satisfies the full native-cost hypothesis package: reciprocal symmetry, normalization invariance, and the Recognition Composition Law on nonzero ratio orbits. Uniqueness and selection arguments for PRC native costs cite it as the baseline countermodel that still obeys the ledger axioms. The proof is a three-field tactic argument reducing each axiom to cross-equality with the on-orbit cost via nonzero case splits and orbit-arithmetic congruence.
Claim. The zero-flat native cost functional $C_0$ satisfies the native-cost hypothesis package: for every ratio orbit $q$, $C_0(q)$ is cross-equivalent to $C_0(q^{-1})$ and to $C_0(\mathrm{normalize}(q))$; and for nonzero orbits $x,y$, the Recognition Composition Law $C_0(xy)+C_0(x/y)=2\,C_0(x)C_0(y)+2\,C_0(x)+2\,C_0(y)$ holds up to internal cross-multiplication equivalence of ratio orbits.
background
In the Primitive Recognition Calculus, ratios live as ratio-orbit objects (signed numerator/denominator delta-orbits). Equality of displayed rationals is the internal relation cross-equality: two orbits are equivalent when cross-multiplication balances as signed orbits. Upstream, cross-equality agrees with ordinary rational equality of verifier displays; reflexivity, symmetry, and transitivity are available as lemmas.
A native cost is a map from ratio orbits to ratio orbits. The hypothesis package asks three things: reciprocal symmetry (cost of $q$ matches cost of the reciprocal orbit), invariance under distinction-normalization of the ratio, and the canonical Recognition Composition Law (RCL) on products and quotients of nonzero orbits. The zero-flat native cost collapses to the zero display on the zero orbit and otherwise tracks the standard on-orbit cost; it is the natural countermodel once zero-orbit calibration is dropped.
Local setting is the PRC native-cost uniqueness module: one builds enough structure on candidate costs to force uniqueness, then uses explicit models that still obey the ledger axioms to refute over-strong targets.
proof idea
The proof fills the three structure fields by tactic.
For reciprocal: case-split on whether $q$ displays as zero. If zero, the reciprocal also displays zero, so both cost sides hit the zero branch and cross-equality is immediate via the toRat characterization. If nonzero, the reciprocal is nonzero; chain transitivity through the nonzero on-orbit agreement lemma, reciprocal symmetry of the underlying cost, and the symmetric nonzero agreement on the reciprocal.
Normalized invariance is the same pattern with normalize in place of reciprocal: zero stays zero; nonzero stays nonzero; transit through nonzero agreement and underlying normalized invariance.
For canonical RCL: assume $x,y$ nonzero. Products and quotients stay nonzero. Build cross-equality between the left-hand RCL combination of zero-flat costs and the on-orbit combination by add-congruence of the two nonzero agreements; likewise for each right-hand multiplicative term via mul-congruence and reflexivity on the constant two. Transit and the underlying on-orbit RCL close the identity.
why it matters
This theorem installs the zero-flat cost as a fully axiom-compliant native cost, so uniqueness targets can use it as a live countermodel. Downstream, the character-trace lift target is refuted by applying any claimed lift to zero-flat, which has no character trace. Likewise the doubled-trace zero-calibration target is refuted by feeding zero-flat into that package.
It also seeds the selection layer: the prime-signed strengthened hypotheses package this result as the native core of the strengthened ledger (everything except zero-orbit calibration). In framework terms this sits under the RCL landmark (the composition law forced at T5 via J-uniqueness): RCL alone, with reciprocal and normalization, does not pin a unique native cost once the zero orbit is free. The open pressure is therefore on zero-calibration and character/trace matching, not on the bare ledger axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.