Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness Prcprime Cal

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness Prcprime Cal

A machine-checked proof shows that if a recognition cost behaves correctly on two and three, it cannot secretly misbehave on composite numbers.

Verify this page

The defect character

The declaration PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_of_two_three_local_orientation_failure_character is a formal statement about a recognition cost, a rule that assigns a price to each step in a discrete record of events. The framework's central cost function, J(x) = (x + 1/x)/2 - 1, is the unique rule satisfying five plain conditions, and this declaration is part of the machine-checked library of formal theorems that verifies that uniqueness holds even when the cost is examined only through its behavior on small prime numbers.

In plain language, the declaration establishes a consistency property. Suppose a cost rule has been calibrated so that it behaves correctly on the prime directions 2 and 3, meaning its values there match the reciprocal symmetry the framework requires. The declaration proves that this local correctness on 2 and 3 rules out a certain kind of hidden defect: a composite cost defect character, a hypothetical cost rule that would agree with the correct one on 2 and 3 but diverge from it on composite numbers. The theorem states that no such defect character exists. Equivalently, the property of excluding that defect is equivalent to the property of excluding a mixed composite cost defect, and both are equivalent to the absence of a non-two mixed character. The proof is a chain of equivalences, each step checked by the machine, so the claim is not a heuristic or a numerical coincidence but a theorem in the library.

The declaration does not claim that the full cost function is derived from the values on 2 and 3 alone. It claims only that a specific defect, one that would break the reciprocal identity on composite numbers while respecting it on 2 and 3, is impossible. It also does not claim that the values on 2 and 3 determine the cost everywhere; that would be a much stronger statement, and the library contains separate theorems showing that the composition law without calibration does not force the unique cost. The declaration is one link in a chain: it closes a loophole, it does not by itself prove the uniqueness theorem.

What this changes for a reader is the shape of the uniqueness argument. The framework's central result, that the cost must equal J(x), is not proved by checking every number. It is proved by showing that the five conditions force a structure that is rigid: once the behavior on the prime directions 2 and 3 is fixed, certain kinds of deviation are simply impossible. This declaration is the formal record of one such impossibility, and it is part of why the uniqueness claim can be stated with confidence rather than as a conjecture.

THEOREM PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_defect_character · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_defect_character · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean:10407 
theorem PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_defect_character :
    PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
      ¬ PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter := by
  constructor
  · intro hexcl hdefect
    exact
      (PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character.mp
        hexcl)
        (PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_composite_defect
          hdefect)
  · intro hdefect
    exact
      PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character.mpr
        (by
          intro hmix
          exact hdefect
            (PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeDefectCharacter_of_non_two_mixed
              hmix))
THEOREM PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean:10362 
theorem PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character :
    PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
      ¬ PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter := by
  constructor
  · intro hexcl hnonTwo
    exact
      (PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_absurd_of_witness_excludes
        hexcl)
        (PRCPrimeCalibratedTwoPrimeReciprocalIdentityPrimeMixedCharacter_of_non_two_mixed
          hnonTwo)
  · intro hnonTwo
    exact
      PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_of_no_mixed_character
        (by
          intro hmix
          exact hnonTwo
            (PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoPrimeMixedCharacter_of_mixed
              hmix))
THEOREM composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean:1703 
/-- **Completion-side non-forcing (headline blocker, stated exactly).**

There is a function `F : ℝ → ℝ` (the `λ = 2` cost `(x² + x⁻²)/2 - 1`) that
satisfies every hypothesis of `law_of_logic_forces_jcost` *except* calibration
(reciprocal symmetry, normalization, the composition law (RCL), and continuity on
the positive reals) yet is not the canonical cost `Cost.Jcost`. Therefore the
calibration hypothesis `IsCalibrated` is load-bearing and cannot be dropped: the
composition law and the other algebraic laws do not, by themselves, force J even
on the continuous completion.

This is the continuum analogue of `prc_native_cost_orientation_underdetermined`
and `prc_single_prime_calibration_insufficient`. Read together: on the rational
carrier orientation is free per prime; on the completion the scale (the curvature
`λ²` at the unit) is free. In both regimes the binding constraint is a
calibration, not the algebra. Consequently "δ forces J" can only mean "δ forces
the cost family `(x^λ + x^{-λ})/2 - 1`, and a separately supplied unit
calibration selects `λ = 1`." Whether δ supplies that unit calibration is the
open joint (live track T1); this theorem proves it is genuinely needed, i.e. it
is not already implied by the composition law. -/
theorem composition_law_without_calibration_does_not_force_jcost :
    ∃ F : ℝ → ℝ,
      Cost.FunctionalEquation.IsReciprocalCost F ∧
      Cost.FunctionalEquation.IsNormalized F ∧
      Cost.FunctionalEquation.SatisfiesCompositionLaw F ∧
      ContinuousOn F (Set.Ioi 0) ∧
      F ≠ Cost.Jcost := by
  refine ⟨costLambdaTwo, ?_, ?_, ?_, ?_, ?_⟩
  · -- reciprocal symmetry
    intro x hx
    have hx0 : x ≠ 0 := ne_of_gt hx
    unfold costLambdaTwo
    field_simp
    ring
  · -- normalization F 1 = 0
    show ((1 : ℝ) ^ 2 + ((1 : ℝ) ^ 2)⁻¹) / 2 - 1 = 0
    norm_num
  · -- composition law (RCL)
    intro x y hx hy
    have hx0 : x ≠ 0 := ne_of_gt hx
    have hy0 : y ≠ 0 := ne_of_gt hy
    unfold costLambdaTwo
    field_simp
    ring
  · -- continuity on the positive reals
    unfold costLambdaTwo
    apply ContinuousOn.sub _ continuousOn_const
    apply ContinuousOn.div_const
    refine ContinuousOn.add ((continuous_pow 2).continuousOn) ?_
    refine ContinuousOn.inv₀ ((continuous_pow 2).continuousOn) ?_
    intro x hx
    exact pow_ne_zero 2 (ne_of_gt (Set.mem_Ioi.mp hx))
  · -- F ≠ Jcost, witnessed at x = 2
    intro h
    have h2 := congrFun h 2
    unfold costLambdaTwo Cost.Jcost at h2
    norm_num at h2

What this page does not claim

The declaration does not claim that the cost function is determined by its values on 2 and 3 alone. It does not claim that the uniqueness theorem for the cost function follows from this declaration alone.

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/PRCNativeCostUniqueness.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