Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Minimality Character Pa

ARTICLE 2 claims 2 theorems

Foundation Primitive Recognition Calculus Prcnative Cost Minimality Character Pa

A machine-checked theorem shows that fixing a cost function's value at the number two forces its values at every prime number, a step in a broader attempt to derive physics from a single forced cost function.

Verify this page

The calibration theorem

The theorem character_pair_two_calibration_forces_prime_calibration is a formal statement inside the Recognition Science framework's machine-checked library of formal theorems. It concerns a cost function, which in this framework is a rule that assigns a number to each possible ratio of two quantities, representing the price of recognizing that ratio. The theorem says: if a cost function satisfies three conditions, then its value at every prime number is forced. The three conditions are that the function is a valid character of the ratio orbits, that it is consistent with the product cost of a prime pair, and that its value at two equals a specific reference value.

The significance is that this is not a claim about the physical world directly, but a structural result within a formal system. The framework's library proves this theorem from its axioms, with no gaps. The theorem is a lemma in a larger chain: the framework aims to show that a single cost function, forced by five plain conditions, leads to constants like the golden ratio and three spatial dimensions. This particular theorem is a step in that chain, showing that a small amount of calibration data, specifically the value at two, propagates to all primes.

What the theorem does not claim is just as important. It does not claim that the cost function's value at two is physically measured or known; that is a separate question. It does not claim that the cost function is unique; other theorems in the library handle uniqueness under stronger hypotheses. And it does not claim that the prime calibration has any direct experimental consequence. The theorem is a piece of pure mathematics within the framework, not a prediction about the universe.

THEOREM character_pair_two_calibration_forces_prime_calibration · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean
character_pair_two_calibration_forces_prime_calibration · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean:147 
/-- **Prime-pair products plus the base two-point calibration force cost
calibration on every native prime axis.** This is the transport the round-1
premise ledger was missing: the all-prime family is not independent data once
the pair field and the base ledger's two-calibration are present. -/
theorem character_pair_two_calibration_forces_prime_calibration
    {χ : RatioOrbit → RatioOrbit}
    (hχ : PRCRatioCharacter χ)
    (hpair : PRCCharacterPrimePairProductCostConsistent χ)
    (htwo : RatioOrbit.crossEq (costFromCharacter χ two) (onRatioOrbit two)) :
    PRCCharacterPrimeDirectionCalibrated χ := by
  intro p hp
  -- displays
  have hPne : (primeDirection p hp).toRat ≠ 0 := primeDirection_toRat_ne_zero p hp
  have hvne : (χ (primeDirection p hp)).toRat ≠ 0 := hχ.nonzero_preserving hPne
  have hPnat : p.toNat ≠ 0 := by
    have h := hPne
    rw [primeDirection_toRat] at h
    exact_mod_cast h
  have hP1 : (1:ℚ) ≤ (p.toNat : ℚ) := by
    exact_mod_cast Nat.one_le_iff_ne_zero.mpr hPnat
  have hPQ : ((p.toNat : ℚ)) ≠ 0 := by
    rw [← primeDirection_toRat p hp]
    exact hPne
  have hpd2Rat : (primeDirection twoOrbit twoOrbit_primeOrbit).toRat = 2 := by
    rw [primeDirection_toRat, twoOrbit_toNat]
    norm_num
  -- the character respects crossEq (native GCD normalization is canonical)
  have hrespect : PRCCharacterRespectsCrossEq χ :=
    PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
      PRCNormalizeRatioCanonicalTarget_proved
  -- transfer the two-point calibration to the two prime direction
  have h2cross :
      RatioOrbit.crossEq two (primeDirection twoOrbit twoOrbit_primeOrbit) := by
    rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat, hpd2Rat]
  have hχtwoEq :
      (χ two).toRat = (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat := by
    have h := hrespect two (primeDirection twoOrbit twoOrbit_primeOrbit) h2cross
    rw [RatioOrbit.crossEq_iff_toRat_eq] at h
    exact h
  -- dichotomy at the two orbit
  have h2ne : (two : RatioOrbit).toRat ≠ 0 := by
    rw [two_toRat]
    norm_num
  have hχ2ne : (χ two).toRat ≠ 0 := hχ.nonzero_preserving h2ne
  have hu :
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2 ∨
        (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2⁻¹ := by
    rcases jcost_eq_forces_same_or_reciprocal hχ2ne h2ne
        (by simpa [costFromCharacter] using htwo) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat] at h
      rw [← hχtwoEq]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat, two_toRat] at h
      rw [← hχtwoEq]
      exact h
  -- dichotomy at the pair (2, p)
  have h2pne :
      (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
        (primeDirection p hp)).toRat ≠ 0 := by
    rw [RatioOrbit.mul_toRat, hpd2Rat]
    exact mul_ne_zero (by norm_num) hPne
  have hmul2p :
      (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
        (primeDirection p hp))).toRat =
        (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat := by
    have h := hχ.multiplicative (primeDirection twoOrbit twoOrbit_primeOrbit)
      (primeDirection p hp)
    rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
    exact h
  have huv :
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat =
        2 * (p.toNat : ℚ) ∨
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat =
        (2 * (p.toNat : ℚ))⁻¹ := by
    have hχ2pne :
        (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
          (primeDirection p hp))).toRat ≠ 0 :=
      hχ.nonzero_preserving h2pne
    rcases jcost_eq_forces_same_or_reciprocal hχ2pne h2pne
        (by simpa [costFromCharacter]
          using hpair twoOrbit twoOrbit_primeOrbit p hp) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat, hpd2Rat,
        primeDirection_toRat] at h
      rw [← hmul2p]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
        RatioOrbit.mul_toRat, hpd2Rat, primeDirection_toRat] at h
      rw [← hmul2p]
      exact h
  -- dichotomy at the pair (p, p)
  have hppne :
      (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp)).toRat ≠ 0 := by
    rw [RatioOrbit.mul_toRat]
    exact mul_ne_zero hPne hPne
  have hmulpp :
      (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat =
        (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat := by
    have h := hχ.multiplicative (primeDirection p hp) (primeDirection p hp)
    rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
    exact h
  have hvv :
      (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
        (p.toNat : ℚ) * (p.toNat : ℚ) ∨
      (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
        ((p.toNat : ℚ) * (p.toNat : ℚ))⁻¹ := by
    have hχppne :
        (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat ≠
          0 :=
      hχ.nonzero_preserving hppne
    rcases jcost_eq_forces_same_or_reciprocal hχppne hppne
        (by simpa [costFromCharacter] using hpair p hp p hp) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat,
        primeDirection_toRat] at h
      rw [← hmulpp]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
        RatioOrbit.mul_toRat, primeDirection_toRat] at h
      rw [← hmulpp]
      exact h
  -- the case split leaves the identity or reciprocal branch
  have hbranch :
      (χ (primeDirection p hp)).toRat = (p.toNat : ℚ) ∨
        (χ (primeDirection p hp)).toRat = ((p.toNat : ℚ))⁻¹ :=
    pair_two_case_split hPQ hP1 hu huv hvv
  -- both branches carry the same J display
  rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_toRat, onRatioOrbit_toRat,
    primeDirection_toRat]
  rcases hbranch with h | h
  · rw [h]
  · rw [h, inv_inv]
    ring
THEOREM character_pair_two_calibration_forces_prime_calibration · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean
character_pair_two_calibration_forces_prime_calibration · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostMinimality.lean:147 
/-- **Prime-pair products plus the base two-point calibration force cost
calibration on every native prime axis.** This is the transport the round-1
premise ledger was missing: the all-prime family is not independent data once
the pair field and the base ledger's two-calibration are present. -/
theorem character_pair_two_calibration_forces_prime_calibration
    {χ : RatioOrbit → RatioOrbit}
    (hχ : PRCRatioCharacter χ)
    (hpair : PRCCharacterPrimePairProductCostConsistent χ)
    (htwo : RatioOrbit.crossEq (costFromCharacter χ two) (onRatioOrbit two)) :
    PRCCharacterPrimeDirectionCalibrated χ := by
  intro p hp
  -- displays
  have hPne : (primeDirection p hp).toRat ≠ 0 := primeDirection_toRat_ne_zero p hp
  have hvne : (χ (primeDirection p hp)).toRat ≠ 0 := hχ.nonzero_preserving hPne
  have hPnat : p.toNat ≠ 0 := by
    have h := hPne
    rw [primeDirection_toRat] at h
    exact_mod_cast h
  have hP1 : (1:ℚ) ≤ (p.toNat : ℚ) := by
    exact_mod_cast Nat.one_le_iff_ne_zero.mpr hPnat
  have hPQ : ((p.toNat : ℚ)) ≠ 0 := by
    rw [← primeDirection_toRat p hp]
    exact hPne
  have hpd2Rat : (primeDirection twoOrbit twoOrbit_primeOrbit).toRat = 2 := by
    rw [primeDirection_toRat, twoOrbit_toNat]
    norm_num
  -- the character respects crossEq (native GCD normalization is canonical)
  have hrespect : PRCCharacterRespectsCrossEq χ :=
    PRCCharacterRespectsCrossEq_of_normalizeRatio_canonical hχ
      PRCNormalizeRatioCanonicalTarget_proved
  -- transfer the two-point calibration to the two prime direction
  have h2cross :
      RatioOrbit.crossEq two (primeDirection twoOrbit twoOrbit_primeOrbit) := by
    rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat, hpd2Rat]
  have hχtwoEq :
      (χ two).toRat = (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat := by
    have h := hrespect two (primeDirection twoOrbit twoOrbit_primeOrbit) h2cross
    rw [RatioOrbit.crossEq_iff_toRat_eq] at h
    exact h
  -- dichotomy at the two orbit
  have h2ne : (two : RatioOrbit).toRat ≠ 0 := by
    rw [two_toRat]
    norm_num
  have hχ2ne : (χ two).toRat ≠ 0 := hχ.nonzero_preserving h2ne
  have hu :
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2 ∨
        (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat = 2⁻¹ := by
    rcases jcost_eq_forces_same_or_reciprocal hχ2ne h2ne
        (by simpa [costFromCharacter] using htwo) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, two_toRat] at h
      rw [← hχtwoEq]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat, two_toRat] at h
      rw [← hχtwoEq]
      exact h
  -- dichotomy at the pair (2, p)
  have h2pne :
      (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
        (primeDirection p hp)).toRat ≠ 0 := by
    rw [RatioOrbit.mul_toRat, hpd2Rat]
    exact mul_ne_zero (by norm_num) hPne
  have hmul2p :
      (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
        (primeDirection p hp))).toRat =
        (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat := by
    have h := hχ.multiplicative (primeDirection twoOrbit twoOrbit_primeOrbit)
      (primeDirection p hp)
    rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
    exact h
  have huv :
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat =
        2 * (p.toNat : ℚ) ∨
      (χ (primeDirection twoOrbit twoOrbit_primeOrbit)).toRat *
          (χ (primeDirection p hp)).toRat =
        (2 * (p.toNat : ℚ))⁻¹ := by
    have hχ2pne :
        (χ (RatioOrbit.mul (primeDirection twoOrbit twoOrbit_primeOrbit)
          (primeDirection p hp))).toRat ≠ 0 :=
      hχ.nonzero_preserving h2pne
    rcases jcost_eq_forces_same_or_reciprocal hχ2pne h2pne
        (by simpa [costFromCharacter]
          using hpair twoOrbit twoOrbit_primeOrbit p hp) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat, hpd2Rat,
        primeDirection_toRat] at h
      rw [← hmul2p]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
        RatioOrbit.mul_toRat, hpd2Rat, primeDirection_toRat] at h
      rw [← hmul2p]
      exact h
  -- dichotomy at the pair (p, p)
  have hppne :
      (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp)).toRat ≠ 0 := by
    rw [RatioOrbit.mul_toRat]
    exact mul_ne_zero hPne hPne
  have hmulpp :
      (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat =
        (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat := by
    have h := hχ.multiplicative (primeDirection p hp) (primeDirection p hp)
    rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat] at h
    exact h
  have hvv :
      (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
        (p.toNat : ℚ) * (p.toNat : ℚ) ∨
      (χ (primeDirection p hp)).toRat * (χ (primeDirection p hp)).toRat =
        ((p.toNat : ℚ) * (p.toNat : ℚ))⁻¹ := by
    have hχppne :
        (χ (RatioOrbit.mul (primeDirection p hp) (primeDirection p hp))).toRat ≠
          0 :=
      hχ.nonzero_preserving hppne
    rcases jcost_eq_forces_same_or_reciprocal hχppne hppne
        (by simpa [costFromCharacter] using hpair p hp p hp) with h | h
    · left
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.mul_toRat,
        primeDirection_toRat] at h
      rw [← hmulpp]
      exact h
    · right
      rw [RatioOrbit.crossEq_iff_toRat_eq, RatioOrbit.recip_toRat,
        RatioOrbit.mul_toRat, primeDirection_toRat] at h
      rw [← hmulpp]
      exact h
  -- the case split leaves the identity or reciprocal branch
  have hbranch :
      (χ (primeDirection p hp)).toRat = (p.toNat : ℚ) ∨
        (χ (primeDirection p hp)).toRat = ((p.toNat : ℚ))⁻¹ :=
    pair_two_case_split hPQ hP1 hu huv hvv
  -- both branches carry the same J display
  rw [RatioOrbit.crossEq_iff_toRat_eq, costFromCharacter_toRat, onRatioOrbit_toRat,
    primeDirection_toRat]
  rcases hbranch with h | h
  · rw [h]
  · rw [h, inv_inv]
    ring

What this page does not claim

The theorem does not claim that the value at two is physically measured or known. The theorem does not claim that the cost function is unique. The theorem does not claim any direct experimental consequence for the prime calibration.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND