Foundation Primitive Recognition Calculus Prcnative Cost Selection Canonical Sel

The canonical cost witness

The declaration canonicalSelectedNativeCost_crossEq_onRatioOrbit is a theorem in the framework's machine-checked library of formal theorems. It states that for every rational ratio q, the value of the canonical selected native cost at q is cross-equal to the value of the raw orbit cost at q. Cross-equal means the two values have the same rational number representation. The theorem is a proof of consistency: the canonical cost, which is the one the framework actually uses, agrees with the underlying orbit cost everywhere, including at the unit ratio where the canonical cost deliberately displays the zero representative.

The theorem is part of a larger uniqueness argument. The framework's library proves that a certain strengthened hypothesis class, the zero-calibrated prime-signed class, has exactly one member up to cross-equality. The canonical cost is the witness that this class is not empty. The theorem canonicalSelectedNativeCost_crossEq_onRatioOrbit is the non-vacuity witness for that uniqueness claim. It shows that the strengthened hypotheses are satisfiable, and that the canonical cost is the intended solution.

The theorem does not claim that the canonical cost is the only possible cost function. It does not claim that the uniqueness result applies to weaker hypothesis classes. The library explicitly proves that the base class, the strengthened class, and the prime-signed strengthened class all fail uniqueness. The theorem also does not claim that the canonical cost is physically realized in nature. It is a mathematical witness within the framework, not an empirical measurement.

In plain terms, the declaration establishes that the framework's chosen cost function is coherent: it picks out one specific function, and that function satisfies the full strengthened conditions. The cost function is not an arbitrary choice, and it is not a vacuous one. The theorem's role is to make the uniqueness result meaningful by showing that the class it characterizes actually contains something.

/-- The selected witness is crossEq-pointwise the canonical cost. -/
theorem canonicalSelectedNativeCost_crossEq_onRatioOrbit (q : RatioOrbit) :
    RatioOrbit.crossEq (canonicalSelectedNativeCost q) (onRatioOrbit q) := by
  rw [RatioOrbit.crossEq_iff_toRat_eq, canonicalSelectedNativeCost_toRat,
    onRatioOrbit_toRat]

/-- The selected witness satisfies the full zero-calibrated prime-signed
strengthened hypothesis class: the frozen ledger is non-vacuous. -/
theorem canonicalSelectedNativeCost_full_hypotheses :
    PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
      canonicalSelectedNativeCost where
  prime_signed :=
    { signed_strengthened :=
        { strengthened :=
            { native := canonicalSelectedNativeCost_native_hypotheses
              prime_pair_product_cost := fun p hp r hr =>
                canonicalSelectedNativeCost_crossEq_onRatioOrbit
                  (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr)) }
          signed_unit :=
            canonicalSelectedNativeCost_crossEq_onRatioOrbit negativeOneRatio }
      prime_direction_cost := fun p hp =>
        canonicalSelectedNativeCost_crossEq_onRatioOrbit (primeDirection p hp) }
  zero_calibrated := by
    rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq]
    simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
      RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
      canonicalSelectedNativeCost_toRat, RatioOrbit.zero_toRat]
    norm_num

/-- The continuum price residue wall holds. -/
theorem continuumPriceResidueWall_holds : ContinuumPriceResidueWall where
  base_insufficient := PRCNativeCostUniquenessTarget_refuted
  strengthened_insufficient := PRCStrengthenedNativeCostUniquenessTarget_refuted
  prime_signed_insufficient :=
    PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted
  every_prime_axis_free := prc_every_prime_axis_orientation_free
  zero_spike_still_excluded := zeroSpikeDoubledTrace_not_zero_calibrated

What this page does not claim

The canonical cost is the only function satisfying the base hypotheses. The canonical cost is an empirically measured quantity. The theorem establishes uniqueness for the prime-signed strengthened class without the zero-calibration condition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostSelection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: