Pith. sign in
theorem

in

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostUniqueness
domain
Foundation
line
1655 · github
papers citing
none yet

plain-language theorem explainer

On the rational carrier, native-cost orientation stays free on every prime axis at once. Cite this when arguing that discrete prime-by-prime calibration cannot pin down the reciprocal cost J. The result lifts the p=2 and p=3 underdetermination witnesses to uniform per-prime freedom, so no proper set of prime calibrations forces the all-identity (canonical) orientation. Continuous completion is required for J-forcing.

Claim. Orientation freedom for the native recognition cost is genuinely per-prime and simultaneous on every prime axis. Hence no finite (indeed, no proper) set of prime calibrations forces the reciprocal cost $J$ on the rational carrier: every axis outside the calibrated set remains free. Canonical $J$ is the all-identity orientation, which discrete arithmetic does not force. Forcing $J$ requires the continuous completion, where calibration constrains a full neighborhood of the unit rather than one axis at a time.

background

In the Primitive Recognition Calculus, a native cost on positive rationals is built from a ratio character and a doubled-trace construction. Reciprocity (invariance under $x \mapsto x^{-1}$) and the Recognition Composition Law constrain the shape of admissible costs, but on the discrete rational carrier those constraints act axis-by-axis along prime valuations.

The reciprocal automorphism of the cost algebra encodes the $x \leftrightarrow x^{-1}$ symmetry. The Law of Logic cost theorem states that $J$ is the unique reciprocal cost satisfying the composition law, normalization, calibration, and continuity: uniqueness uses a global smoothness package and a calibration hypothesis that pins a neighborhood of the unit, not a single prime axis.

Earlier module witnesses already showed underdetermination at $p=2$ and insufficiency of single-prime calibration at $p=3$. The present statement packages the general pattern: orientation choice is free on every prime simultaneously.

proof idea

No proof body is supplied in the extract (zero body lines). From the surrounding narrative and sibling names, the argument is a uniform lift of the existing $p=2$ orientation-underdetermined witness and the $p=3$ single-prime-calibration-insufficient witness: one exhibits, for each prime axis outside any fixed proper set of calibrated primes, an independent orientation flip that preserves the native discrete hypotheses (reciprocity, composition on rationals, and the calibrated axes) while changing the cost off those axes. The canonical all-identity orientation is thereby shown not to be singled out by any proper set of prime calibrations. Continuous J-uniqueness is deferred to law_of_logic_forces_jcost, whose calibration hypothesis acts on a neighborhood of the unit.

why it matters

This is the discrete negative counterpart to T5 J-uniqueness and to the Law of Logic cost theorem. It explains why the forcing chain cannot close on $\mathbb{Q}_{>0}$ alone: prime-axis orientations remain free, so the canonical reciprocal cost $J(x)=(x+x^{-1})/2-1$ is not selected by discrete arithmetic. J-forcing must pass through continuous completion, where calibration constrains a full neighborhood of the unit at once.

No downstream consumers are recorded in the graph for this declaration. Its role is foundational hygiene inside PRC native-cost uniqueness: it blocks the false hope that finitely many prime calibrations, or any proper set of them, could replace the continuity-plus-calibration package. Open edge: the precise bridge from this per-prime freedom to the Aczél/smoothness hypotheses used in the continuous uniqueness theorem.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.