Foundation Primitive Recognition Calculus Prcnative Cost Selection Zero Flat Nat

The zero-flat cost witness

In the Recognition Science framework, a cost is a rule that assigns a price to every possible recognition event, where a recognition event is the act of comparing one quantity with another. The framework's central question is which cost functions are forced by its axioms. The declaration zeroFlatNativeCost_prime_signed_strengthened_hypotheses establishes that a particular cost function, called the zero-flat native cost, satisfies the framework's strongest zero-calibrated, prime-signed, strengthened hypothesis class. This is a machine-checked theorem in the framework's library of formal theorems, meaning the proof is verified by a computer.

The zero-flat native cost is defined by the formula J(x) = (x + 1/x)/2 - 1 for all ratios x, except that when x equals 1, the cost is set to the literal zero representative rather than the structurally distinct but equivalent representative 0/2. This routing to the canonical zero representative is what makes the cost satisfy the unit-zero field of the strengthened hypotheses. The same declaration also proves that two simpler candidate costs, the constant-zero cost and the linear cost, are excluded from this hypothesis class, because they fail the two-calibration condition.

The significance of this witness is that it shows the strengthened hypothesis class is not vacuous: there exists at least one cost function that satisfies all the axioms. However, the pack also contains a companion theorem, PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted, which proves that the uniqueness target for this class is false. In plain language, the strengthened axioms do not force a unique cost function; the zero-flat cost is one witness, but the uniqueness claim fails. This is part of a broader pattern in the framework's ledger, where the continuum price residue wall records that even the prime-signed strengthened hypotheses are insufficient for uniqueness.

What this declaration does not claim is that the zero-flat cost is the only cost satisfying the strengthened hypotheses, nor that it is the physically realized cost in the framework's derivation chain. It only establishes that the hypothesis class has at least one member, the zero-flat cost, and that this member is distinct from the excluded constant-zero and linear candidates. The uniqueness failure is a separate, explicitly proved result, not a consequence of the witness declaration itself.

/-- The zero-flat countermodel satisfies the prime-signed strengthened ledger
(everything except zero-orbit calibration). -/
theorem zeroFlatNativeCost_prime_signed_strengthened_hypotheses :
    PRCPrimeSignedStrengthenedNativeCostHypotheses zeroFlatNativeCost where
  signed_strengthened :=
    { strengthened :=
        { native := zeroFlatNativeCost_hypotheses
          prime_pair_product_cost := by
            intro p hp r hr
            refine zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero ?_
            rw [RatioOrbit.mul_toRat]
            exact mul_ne_zero (primeDirection_toRat_ne_zero p hp)
              (primeDirection_toRat_ne_zero r hr) }
      signed_unit := by
        refine zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero ?_
        rw [negativeOneRatio_toRat]
        norm_num }
  prime_direction_cost := fun p hp =>
    zeroFlatNativeCost_crossEq_onRatioOrbit_of_nonzero
      (primeDirection_toRat_ne_zero p hp)

/-- The canonical selected native cost: the J cost with the unit orbit sent to
the literal zero representative. This is the non-vacuity witness for the full
zero-calibrated prime-signed strengthened hypothesis class. -/
def canonicalSelectedNativeCost (q : RatioOrbit) : RatioOrbit :=
  if q.toRat = 1 then RatioOrbit.zero else onRatioOrbit q

/-- **Zero-orbit calibration is irreducible.** Without it, the prime-signed
strengthened ledger admits the zero-flat countermodel: uniqueness fails at the
zero orbit, where the canonical cost displays `-1` and the countermodel
displays `0`. -/
theorem PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted :
    ¬ PRCPrimeSignedStrengthenedNativeCostUniquenessTarget := by
  intro h
  have hzero :=
    h zeroFlatNativeCost zeroFlatNativeCost_prime_signed_strengthened_hypotheses
      RatioOrbit.zero
  rw [zeroFlatNativeCost_zero, RatioOrbit.crossEq_iff_toRat_eq,
    RatioOrbit.zero_toRat, onRatioOrbit_toRat, RatioOrbit.zero_toRat] at hzero
  norm_num at hzero

/-- Decoy exclusion 1 against the full frozen class. -/
theorem constantZeroNativeCost_excluded :
    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
        constantZeroNativeCost :=
  fun h =>
    constantZeroNativeCost_not_native_hypotheses
      h.prime_signed.signed_strengthened.strengthened.native

/-- Decoy exclusion 2 against the full frozen class. -/
theorem linearNativeCost_excluded :
    ¬ PRCZeroCalibratedPrimeSignedStrengthenedNativeCostHypotheses
        linearNativeCost :=
  fun h =>
    linearNativeCost_not_native_hypotheses
      h.prime_signed.signed_strengthened.strengthened.native

What this page does not claim

The zero-flat cost is the unique cost satisfying the strengthened hypotheses. The zero-flat cost is the physically realized cost in the framework's derivation chain. The uniqueness failure is a consequence of the witness declaration itself; it is a separate proved result.

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: