Foundation Primitive Recognition Calculus Prcnative Cost Minimality Prczero Cali

The zero-calibrated uniqueness proof

In the Recognition Science framework, a ledger, a discrete record of recognition events, assigns a cost to each possible ratio between two recognized quantities. The question is whether the framework's conditions force a single, unique cost function. The declaration PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved is a machine-checked theorem that answers yes: under a specific strengthened set of hypotheses, any cost function F must be the identity, meaning F(q) = q for every ratio q. This is not a numerical approximation or a heuristic; it is a formal proof in the framework's machine-checked library of formal theorems.

The theorem's strength comes from its hypotheses. The strengthened conditions require the cost function to be signed, meaning it distinguishes between a ratio and its reciprocal, and zero-calibrated, meaning the cost of the doubled trace at the zero orbit is fixed. These extra constraints rule out the counterexamples that defeat a weaker, unsigned version of the uniqueness claim. The proof also shows that the canonical cost function, the one the framework selects, satisfies all these hypotheses, so the uniqueness result is not vacuous: a valid example exists.

The declaration does not claim uniqueness for the simpler, unstrengthened ledger. A separate theorem in the same file, PRCSignedStrengthenedNativeCostUniquenessTarget_refuted, proves the opposite: without the zero-calibration condition, the uniqueness target is false. The counterexample is a zero-flat cost function, one that assigns zero cost to every nonzero orbit. This function satisfies the signed conditions but not the zero-calibrated one, and it breaks uniqueness. The strengthened theorem therefore does real work: it identifies exactly which additional condition is needed to force the identity.

In Recognition Science, this result is a step toward showing that the framework's cost function is not arbitrary. The framework models recognition as a forced process, and this theorem supports that picture by showing that a natural set of constraints leaves no room for choice. The practical upshot is a sharper boundary: the framework knows precisely which premises are load-bearing and which are not. That boundary is the theorem's real contribution, more than the identity conclusion itself.

/-- **The slim ledger already forces J.** Factorization needs only base + zero;
the pair and sign fields transfer to the factor character; the new transport
lemma recovers per-prime calibration from the pair field and the base
two-calibration; the existing signed-admissible rigidity closes. -/
theorem PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved :
    PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget := by
  intro F hF q
  rcases PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F
      hF.signed_strengthened.strengthened.native hF.zero_calibrated with
    ⟨χ, hχ, hFχ⟩
  have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
    intro p hp r hr
    exact RatioOrbit.crossEq_trans
      (RatioOrbit.crossEq_symm
        (hFχ (RatioOrbit.mul (primeDirection p hp) (primeDirection r hr))))
      (hF.signed_strengthened.strengthened.prime_pair_product_cost p hp r hr)
  have htwoCal :
      RatioOrbit.crossEq (costFromCharacter χ two) (onRatioOrbit two) :=
    RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ two))
      hF.signed_strengthened.strengthened.native.two_calibrated
  have hprime : PRCCharacterPrimeDirectionCalibrated χ :=
    character_pair_two_calibration_forces_prime_calibration hχ hpair htwoCal
  have hsignCost :
      RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
        (onRatioOrbit negativeOneRatio) :=
    RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
      hF.signed_strengthened.signed_unit
  have hsign : PRCCharacterSignedUnitCalibrated χ :=
    costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
  exact RatioOrbit.crossEq_trans (hFχ q)
    (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
      ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)

/-- The round-1 non-vacuity witness inhabits the slim class. -/
theorem canonicalSelectedNativeCost_slim_hypotheses :
    PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
      canonicalSelectedNativeCost :=
  (slim_class_iff_full_class canonicalSelectedNativeCost).mpr
    canonicalSelectedNativeCost_full_hypotheses

/-- **The launch prompt's named target is refuted.** The signed-strengthened
ledger (base + pairs + signed unit, no zero field) admits the zero-flat
countermodel: every one of its fields lives on nonzero orbits. -/
theorem PRCSignedStrengthenedNativeCostUniquenessTarget_refuted :
    ¬ PRCSignedStrengthenedNativeCostUniquenessTarget := by
  intro h
  have hzero :=
    h zeroFlatNativeCost
      zeroFlatNativeCost_prime_signed_strengthened_hypotheses.signed_strengthened
      RatioOrbit.zero
  rw [zeroFlatNativeCost_zero, RatioOrbit.crossEq_iff_toRat_eq,
    RatioOrbit.zero_toRat, onRatioOrbit_toRat, RatioOrbit.zero_toRat] at hzero
  norm_num at hzero

/-- Layer discrimination: the zero-flat cost passes every slim field except
the zero orbit (round-1 theorem gives it the larger prime-signed class), and
fails the slim class exactly there. -/
theorem zeroFlatNativeCost_slim_excluded :
    ¬ PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses
        zeroFlatNativeCost := by
  intro h
  have hz := h.zero_calibrated
  rw [PRCDoubledTraceZeroCalibrated, RatioOrbit.crossEq_iff_toRat_eq] at hz
  simp only [nativeCostDoubledTrace, doubledTraceValue, zeroFlatNativeCost_zero,
    RatioOrbit.mul_toRat, RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat,
    RatioOrbit.zero_toRat] at hz
  norm_num at hz

What this page does not claim

The theorem does not prove uniqueness for the unstrengthened, unsigned ledger, which is refuted by the zero-flat counterexample. It does not establish that the identity cost function is the one realized in physical recognition, only that the hypotheses force it. It does not claim that the zero-calibration condition is physically necessary, only that it is mathematically sufficient for uniqueness.

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/PRCNativeCostMinimality.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: