zeroFlatNativeCost_prime_signed_strengthened_hypotheses
plain-language theorem explainer
The zero-flat cost satisfies every axiom of the prime-signed strengthened native-cost ledger except zero-orbit calibration. Anyone arguing that uniqueness needs an explicit zero-orbit condition cites this countermodel certificate. The proof assembles the hypothesis bundle by reducing cross-equality on nonzero ratio orbits to the zero-flat identity and checking the signed unit and prime directions.
Claim. The zero-flat native cost $C_0$ satisfies the prime-signed strengthened native-cost hypotheses: it obeys the native ledger axioms, the prime-pair product cost identity on nonzero ratio orbits, the signed-unit cross-equality at the negative-one ratio, and the prime-direction cost identity for every prime direction.
background
In the Primitive Recognition Calculus, native costs are candidate recognition costs on ratio orbits. The selection program asks which axioms force the canonical cost (tied to the J-cost $J(x)=(x+x^{-1})/2-1$) and exclude competitors. A strengthened ledger adds pair-product and signed-unit constraints on top of the base native axioms; the prime-signed variant further requires cost identities along prime directions.
The zero-flat native cost is the constant-zero competitor on the relevant orbits. Downstream uniqueness targets fail precisely when zero-orbit calibration is omitted, because $C_0$ still meets every nonzero-orbit constraint while disagreeing with the canonical cost at the zero orbit (canonical value $-1$, zero-flat value $0$).
Upstream cost language is the usual recognition cost: observer cost is J-cost of the event state, and multiplicative-recognizer cost is the derived comparator cost on positive ratios. The present lemma only needs the zero-flat cross-equality lemma on nonzero ratio orbits, plus nonvanishing of prime-direction and negative-one rational images.
proof idea
Tactic proof that fills the prime-signed strengthened hypothesis structure for zero-flat cost.
- Native block: reuse the already-proved zero-flat native hypotheses.
- Prime-pair product cost: for primes $p,r$, reduce via the zero-flat cross-equality-on-nonzero-orbits lemma; nonvanishing of the product orbit follows from
RatioOrbit.mul_toRatand nonvanishing of each prime direction in $\mathbb{Q}$. - Signed unit: same cross-equality lemma at the negative-one ratio, after rewriting its rational image and a
norm_numnonvanishing check. - Prime-direction cost: direct application of the nonzero-orbit cross-equality lemma using prime-direction nonvanishing.
why it matters
This is the countermodel certificate that makes zero-orbit calibration irreducible in the native-cost selection chain. Downstream, PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted applies it at the zero orbit to show uniqueness fails without that calibration: canonical cost shows $-1$ there while zero-flat shows $0$. The same bundle feeds the signed-strengthened uniqueness refutation (every field of that weaker ledger lives on nonzero orbits) and sits under the slim cost-selection package that restores uniqueness only after zero calibration is restored.
In framework terms this protects T5-style J-uniqueness: the Recognition Composition Law and J-cost selection are not forced by prime/signed nonzero-orbit axioms alone. The zero orbit is an independent forcing site, not a corollary of prime directions or the signed unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.