continuumPriceResidueWall_holds
plain-language theorem explainer
The continuum-price residue wall holds: every finite strengthening of the δ-native cost ledger still fails uniqueness, so the continuum price of ContinuousOn plus one-point calibration cannot be bought by a finite native family. Cite this when arguing that J-cost uniqueness on the continuum forces an infinite independent calibration residue on the discrete carrier. The proof is a pure structure pack of five already-proved refutations and orientation-freedom lemmas.
Claim. The continuum-price residue wall is inhabited: the base native-cost uniqueness target fails; the strengthened (prime-pair product) target fails; the prime-signed strengthened target fails; for every prime orbit there exists a PRC ratio character that inverts that axis while fixing all other prime axes; and the zero-spike doubled-trace countermodel remains excluded from zero-calibration.
background
In the Primitive Recognition Calculus, native costs live on ratio orbits of distinction naturals. The continuum theorem law_of_logic_forces_jcost obtains the unique J-cost $J(x)=(x+x^{-1})/2-1$ from continuity plus a single calibration point. On the δ-native carrier that continuum package is not free: each finite ledger of algebraic constraints still leaves countermodels.
ContinuumPriceResidueWall packages that irreducible residue (prereg PREREG-jfree-mint-20260724). Its fields are kernel-checked negations: the base uniqueness target admits a two-adic axis twist; adding prime-pair products still fails; the prime-signed strengthening still fails at the zero orbit (canonical cost $-1$ versus countermodel $0$); and orientation freedom holds on every prime axis at once.
Upstream, prc_every_prime_axis_orientation_free is the headline non-forcing statement: for every prime orbit $p$ there is a PRC ratio character fixing all other prime axes and inverting the $p$-axis. The prime-signed refutation shows zero-orbit calibration is irreducible without an extra hypothesis.
proof idea
Term-mode structure constructor. Each field of ContinuumPriceResidueWall is filled by a named upstream theorem: base insufficiency by the base uniqueness refutation; strengthened insufficiency by the strengthened uniqueness refutation; prime-signed insufficiency by the zero-flat countermodel refutation at the zero orbit; every-prime-axis freedom by the classified orientation-freedom theorem; zero-spike exclusion by the doubled-trace non-calibration lemma. No new arithmetic is performed here.
why it matters
This is the honest deposit that the continuum price of J-uniqueness (forcing-chain T5) leaves a permanent residue on the δ-native side. Downstream, continuum_price_residue_wall_tagged wraps the wall at strength tag classicalExtension (panel K2), because the countermodel characters are classical verifier-side constructions. The same fact enters nativeCostSelectionPremiseLedger_all_deltaOnly, which certifies that the selection premise ledger sits uniformly at the δ-only floor.
Framework role: it separates what continuity buys in one stroke from what a discrete native ledger must purchase as an infinite independent calibration family. It does not itself select the canonical native cost; it only walls off every finite uniqueness claim short of that infinite family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.