Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Even

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcnative Cost Structural Ledger Even

A machine-checked proof shows that a cost function built from squaring ratios is the unique one satisfying a short list of structural conditions, and that dropping one condition makes uniqueness fail.

Verify this page

The even-power cost

The declaration evenPowerGeneratedNativeCost defines a specific cost function on positive rational ratios. In plain terms, it assigns a cost to a ratio x by squaring it, taking the reciprocal square, averaging those two numbers, and subtracting 1. This is the even-power analogue of the framework's central cost function J(x) = (x + x⁻¹)/2 - 1, where the exponent 2 replaces 1.

The key theorem about this function, PRCStructuralNativeCostUniquenessTarget_proved, states that if any cost function F on positive rational ratios satisfies the structural hypotheses (reciprocal symmetry, zero cost at 1, a composition law, calibration, and continuity), then F must equal the even-power cost at every ratio. The proof is machine-checked in the framework's library of formal theorems. A companion theorem, structural_forces_positive, shows that any such F assigns a nonnegative cost to every positive ratio.

The interesting negative result concerns the condition called sign-reversing, which forces the cost of a negative ratio to be the negative of the cost of its positive counterpart. If this condition is dropped, uniqueness fails: the theorem PRCStructuralSansAnchorUniquenessTarget_refuted exhibits a different cost function, cubeGeneratedNativeCost, that satisfies all the remaining structural hypotheses but does not equal the even-power cost. So the sign-reversing condition is not decorative; it is load-bearing for the uniqueness conclusion.

What the declaration does not claim: it does not claim that the even-power cost is the one realized in physical recognition events. The framework's physical cost is J(x) = (x + x⁻¹)/2 - 1, not its even-power cousin. The even-power result is a structural theorem about a family of cost functions, not a statement about which cost nature uses. It also does not claim that the even-power cost is unique without the sign-reversing condition; the refutation theorem shows the opposite.

THEOREM PRCStructuralNativeCostUniquenessTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
PRCStructuralNativeCostUniquenessTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:687 
/-- **Round 5 terminal.** The structural ledger forces the canonical cost. -/
theorem PRCStructuralNativeCostUniquenessTarget_proved :
    PRCStructuralNativeCostUniquenessTarget := by
  intro F hF q
  obtain ⟨χ, hχ, hFχ⟩ :=
    PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved F hF.native
      hF.zero_calibrated
  have hcal := structural_character_calibrated_on_positive_integers hF hχ hFχ
  have hresp : PRCCharacterRespectsCrossEq χ :=
    PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
      PRCNormalizeRatioCanonicalTarget_proved
  have hchi : ∀ a b : RatioOrbit, a.toRat = b.toRat →
      (χ a).toRat = (χ b).toRat := by
    intro a b hab
    exact crossDisp
      (hresp a b (dispCross hab))
  -- every positive integer orbit is calibrated
  have hposcal : ∀ (a : RatioOrbit), IsPosIntOrbit a →
      RatioOrbit.crossEq (costFromCharacter χ a) (onRatioOrbit a) := by
    rintro a ⟨n, hn, han⟩
    have hdisp : a.toRat = (natOrbit n).toRat := by rw [natOrbit_toRat, han]
    rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_jq, jq_onRatioOrbit,
      han]
    have hn' := hcal n hn
    rw [← hchi a (natOrbit n) hdisp] at hn'
    exact hn'
  have hprime : PRCCharacterPrimeDirectionCalibrated χ := fun p hp =>
    hposcal _ (primeDirection_isPosInt hp)
  have hpair : PRCCharacterPrimePairProductCostConsistent χ := by
    intro p hp r hr
    refine hposcal _ ⟨p.toNat * r.toNat, ?_, ?_⟩
    · obtain ⟨a, ha, _⟩ := primeDirection_isPosInt hp
      obtain ⟨b, hb, _⟩ := primeDirection_isPosInt hr
      have hpn : 1 ≤ p.toNat := by
        have h := primeDirection_toRat_ne_zero p hp
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      have hrn : 1 ≤ r.toNat := by
        have h := primeDirection_toRat_ne_zero r hr
        rw [primeDirection_toRat] at h
        exact Nat.one_le_iff_ne_zero.mpr (by exact_mod_cast h)
      exact Nat.one_le_iff_ne_zero.mpr (Nat.mul_ne_zero (by omega) (by omega))
    · rw [RatioOrbit.mul_toRat, primeDirection_toRat, primeDirection_toRat]
      push_cast
      ring
  have hsignCost :
      RatioOrbit.crossEq (costFromCharacter χ negativeOneRatio)
        (onRatioOrbit negativeOneRatio) :=
    RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm (hFχ negativeOneRatio))
      (signReversing_forces_signed_unit hF.native.unit_zero hF.sign_reversing)
  have hsign : PRCCharacterSignedUnitCalibrated χ :=
    costFromCharacter_negativeOne_forces_signed_unit hχ hsignCost
  exact RatioOrbit.crossEq_trans (hFχ q)
    (PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved χ
      ⟨⟨hχ, hprime, hpair⟩, hsign⟩ q)
THEOREM PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
PRCStructuralSansAnchorUniquenessTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:1080 
/-- **The anchor is a genuine unit gauge.** The anchor-free structural ledger
does NOT force the canonical cost. Everything else in the ledger is structure;
the last field is a choice of unit. -/
theorem PRCStructuralSansAnchorUniquenessTarget_refuted :
    ¬ PRCStructuralSansAnchorUniquenessTarget := by
  intro huniq
  exact cubeGeneratedNativeCost_two_not_canonical
    (huniq cubeGeneratedNativeCost cubeGeneratedNativeCost_sansAnchor two)
THEOREM structural_forces_positive · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean
structural_forces_positive · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostStructuralLedger.lean:768 
/-- **Positivity is a theorem, not an axiom.** Recognizing a positive imbalance
never pays. -/
theorem structural_forces_positive (F : RatioOrbit → RatioOrbit)
    (hF : PRCStructuralNativeCostHypotheses F) :
    PRCNativeCostPositive F := by
  intro q hq
  have hJ := crossDisp
    (PRCStructuralNativeCostUniquenessTarget_proved F hF q)
  rw [hJ, jq_onRatioOrbit]
  exact jq_nonneg hq

What this page does not claim

The even-power cost is the physical cost realized in recognition events; the framework's physical cost is J(x) = (x + x⁻¹)/2 - 1. The even-power cost is unique without the sign-reversing condition; the refutation theorem shows it is not. The structural hypotheses are independent; some may be consequences of others.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND