ContinuumPriceResidueWall
plain-language theorem explainer
Packages five kernel-checked obstructions showing that δ-native cost uniqueness cannot be bought by any finite calibration ledger that the continuum theorem gets for free from continuity plus one-point fix. Anyone citing the native J-cost selection path or the classical-extension residue wall will use this bundle. It is a pure Prop structure: no proof body, only field names for the five insufficiency and freedom statements.
Claim. The continuum-price residue wall is the conjunction of: (i) the base native-cost uniqueness target fails; (ii) the strengthened (prime-pair) uniqueness target fails; (iii) the prime-signed strengthened uniqueness target fails; (iv) for every prime orbit $p$ there exists a ratio character $\chi$ that fixes every other prime axis under cross-equality and moves the $p$-axis; (v) the zero-spike doubled-trace decoy still fails the doubled-trace zero calibration.
background
In the Primitive Recognition Calculus, costs act on ratio orbits: pairs of a signed numerator orbit and a nonzero distinction-orbit denominator, compared by cross-multiplication balance rather than real equality. Native cost uniqueness targets ask that every admissible cost $F$ agree with the canonical on-orbit cost under that cross-equality, for all ratio orbits.
The continuum side of RS obtains $J$-uniqueness from continuity on the positive reals plus a one-point calibration (the forcing chain's T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). On the $\delta$-native carrier there is no topology to supply that free rigidity, so uniqueness must be purchased by explicit calibration hypotheses on prime axes, signs, pairs, and the zero orbit.
Upstream ingredients include prime-orbit predicates on distinction naturals, ratio characters, cross-equality, and the successive uniqueness targets (base, strengthened, prime-signed strengthened) together with the doubled-trace zero calibration that excludes the zero-spike decoy.
proof idea
No proof: this is a structure declaration of type Prop whose five fields are named hypotheses. Instantiation is deferred to the sibling theorem that fills each field by an existing refutation or freedom lemma (base and strengthened uniqueness refuted, prime-signed strengthened uniqueness refuted, every-prime-axis orientation freedom, and zero-spike exclusion under doubled-trace zero calibration).
why it matters
This is the honest ledger of what the continuum still owes the native carrier: an infinite independent calibration family, one free orientation per prime axis, plus a separate zero-orbit fix. Downstream, continuumPriceResidueWall_holds witnesses the wall by plugging in the five kernel theorems, and continuum_price_residue_wall_tagged deposits it on the public spine at classical-extension strength (countermodels are verifier-side).
In framework terms it separates T5-style $J$-uniqueness on $\mathbb{R}_{>0}$ from what PRC can prove internally. The doc flags an open subquestion: whether a proper subfamily of the cost-level prime calibrations already suffices once pairs and sign are present, since $J$'s reciprocity can hide a single-axis twist on its own axis. The wall is the design requirement that native selection must not pretend continuum continuity is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.