Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness Prcstrengthe
ARTICLE 3 claims 3 theorems
Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness Prcstrengthe
A machine-checked library of formal theorems maps out exactly which extra conditions force a unique cost function in Recognition Science, and which combinations fail.
The strengthened uniqueness target
The declaration PRCStrengthenedNativeCostUniquenessTarget_of_character_factorization_two_calibration_admissible_prime_coherence_and_global_propagation is a target statement in the framework's machine-checked library of formal theorems. It asserts that if a cost function satisfies a specific set of strengthened conditions, then it must be the unique canonical cost. The conditions involve a ratio character, a factorization property, a two-point calibration, and a global propagation condition. The library does not prove this target holds; it proves that certain related targets are false, which maps the boundary of what can be forced.
The library contains several refuted theorems, meaning they are proven false. For example, PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted shows that prime calibration alone does not force a nonunit reciprocal branch transport property. Similarly, PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted and PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted show that other global propagation targets are also false. These refutations are proven theorems; they establish that the strengthened target is not a consequence of the listed conditions alone.
The library also proves equivalences. For instance, PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character shows that a certain exclusion property is equivalent to the absence of a mixed character. Another equivalence, PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency, links it to a consistency condition on composite costs. These equivalences are proven theorems, but they do not establish the strengthened uniqueness target itself.
What the declaration does not claim is that the strengthened target is proved. The target is a statement of what would need to be true for uniqueness under the strengthened conditions. The library's theorems show that some related targets are false, which means the conditions are not sufficient as stated. The uniqueness of the canonical cost function under the original five conditions is a separate, proved theorem. This strengthened target is a different, open question about whether additional conditions can force uniqueness in a broader setting.
THEOREM PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted · PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted · PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
theorem PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted :
¬ PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget := by
intro htarget
have hprime :
PRCCharacterPrimeDirectionCalibrated twoAdicAxisTwistCharacter :=
PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist
twoAdicAxisTwistCharacter_branch
have htransport :
PRCCharacterNonunitReciprocalBranchTransport twoAdicAxisTwistCharacter :=
htarget twoAdicAxisTwistCharacter twoAdicAxisTwistCharacter_ratio_character
hprime
have htwoRec :
PRCCharacterOrbitDirectionReciprocal twoAdicAxisTwistCharacter
twoOrbit twoOrbit_primeOrbit.1 := by
simpa [PRCCharacterOrbitDirectionReciprocal, twoPrimeDirection,
primeDirection] using twoAdicAxisTwistCharacter_branch.1
have hthreeRec :
PRCCharacterOrbitDirectionReciprocal twoAdicAxisTwistCharacter
threeOrbit threeOrbit_primeOrbit.1 :=
htransport twoOrbit twoOrbit_primeOrbit.1 twoOrbit_primeOrbit.2.1 htwoRec
threeOrbit threeOrbit_primeOrbit.1 threeOrbit_primeOrbit.2.1
have hthreeId :
PRCCharacterOrbitDirectionIdentity twoAdicAxisTwistCharacter
threeOrbit threeOrbit_primeOrbit.1 := by
simpa [PRCCharacterOrbitDirectionIdentity, threePrimeDirection,
primeDirection] using
twoAdicAxisTwistCharacter_branch.2 threeOrbit threeOrbit_primeOrbit
threeOrbit_ne_twoOrbit
have hself :
RatioOrbit.crossEq (orbitDirection threeOrbit threeOrbit_primeOrbit.1)
(RatioOrbit.recip (orbitDirection threeOrbit threeOrbit_primeOrbit.1)) :=
RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm hthreeId) hthreeRec
exact orbitDirection_nonunit_not_crossEq_recip threeOrbit
threeOrbit_primeOrbit.1 threeOrbit_primeOrbit.2.1 hself
theorem PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted :
¬ PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget := by
intro htarget
exact PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_refuted
(PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_no_mixed_prime_orientation.mp
htarget)
theorem PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted :
¬ PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget := by
intro htarget
exact PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_refuted
(PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_identity_trace_connected.mp
htarget)
THEOREM PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character · PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
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 PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency :
PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔
PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget := by
constructor
· intro hexcl
exact
PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_of_no_composite_cost_defect
(PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character.mp
hexcl)
· intro hconsistency
exact
PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character.mpr
(PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_absurd_of_mixed_composite_consistency
hconsistency)
THEOREM composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
/-- **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 strengthened uniqueness target itself is not proved in the library. The refuted theorems do not show the canonical cost function is wrong; they show certain stronger conditions fail. The library does not claim that the strengthened conditions are consistent with each other.
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:
- What additional condition would make the strengthened uniqueness target provable?
- Which of the refuted targets could be repaired by adding a single new axiom?
- Is the strengthened target independent of the standard axioms of the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted · PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted · PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
theorem PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted : ¬ PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget := by intro htarget have hprime : PRCCharacterPrimeDirectionCalibrated twoAdicAxisTwistCharacter := PRCCharacterPrimeDirectionCalibrated_of_two_adic_axis_twist twoAdicAxisTwistCharacter_branch have htransport : PRCCharacterNonunitReciprocalBranchTransport twoAdicAxisTwistCharacter := htarget twoAdicAxisTwistCharacter twoAdicAxisTwistCharacter_ratio_character hprime have htwoRec : PRCCharacterOrbitDirectionReciprocal twoAdicAxisTwistCharacter twoOrbit twoOrbit_primeOrbit.1 := by simpa [PRCCharacterOrbitDirectionReciprocal, twoPrimeDirection, primeDirection] using twoAdicAxisTwistCharacter_branch.1 have hthreeRec : PRCCharacterOrbitDirectionReciprocal twoAdicAxisTwistCharacter threeOrbit threeOrbit_primeOrbit.1 := htransport twoOrbit twoOrbit_primeOrbit.1 twoOrbit_primeOrbit.2.1 htwoRec threeOrbit threeOrbit_primeOrbit.1 threeOrbit_primeOrbit.2.1 have hthreeId : PRCCharacterOrbitDirectionIdentity twoAdicAxisTwistCharacter threeOrbit threeOrbit_primeOrbit.1 := by simpa [PRCCharacterOrbitDirectionIdentity, threePrimeDirection, primeDirection] using twoAdicAxisTwistCharacter_branch.2 threeOrbit threeOrbit_primeOrbit threeOrbit_ne_twoOrbit have hself : RatioOrbit.crossEq (orbitDirection threeOrbit threeOrbit_primeOrbit.1) (RatioOrbit.recip (orbitDirection threeOrbit threeOrbit_primeOrbit.1)) := RatioOrbit.crossEq_trans (RatioOrbit.crossEq_symm hthreeId) hthreeRec exact orbitDirection_nonunit_not_crossEq_recip threeOrbit threeOrbit_primeOrbit.1 threeOrbit_primeOrbit.2.1 hselftheorem PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted : ¬ PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget := by intro htarget exact PRCPrimeCalibrationForcesNoMixedPrimeOrientationTarget_refuted (PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_iff_no_mixed_prime_orientation.mp htarget)theorem PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted : ¬ PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget := by intro htarget exact PRCPrimeCalibrationForcesTwoPrimeIdentityTraceConnectedTarget_refuted (PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_iff_identity_trace_connected.mp htarget)The library contains several refuted theorems, meaning they are proven false. PRCPrimeCalibrationForcesNonunitReciprocalBranchTransportTarget_refuted · PRCPrimeCalibrationForcesPrimeReciprocalWitnessGlobalizesTarget_refuted · PRCPrimeCalibrationForcesTwoPrimeReciprocalTraceConnectedTarget_refuted · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.leanTHEOREM PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character · PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
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 PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency : PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget ↔ PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget := by constructor · intro hexcl exact PRCPrimeCalibrationForcesTwoPrimeMixedCompositeCostConsistencyTarget_of_no_composite_cost_defect (PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character.mp hexcl) · intro hconsistency exact PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_composite_cost_defect_character.mpr (PRCPrimeCalibratedTwoPrimeReciprocalIdentityNonTwoCompositeCostDefectCharacter_absurd_of_mixed_composite_consistency hconsistency)The library also proves equivalences. PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_no_non_two_mixed_character · PRCPrimeCalibrationForcesTwoPrimeReciprocalExcludesPrimeIdentityWitnessTarget_iff_mixed_composite_cost_consistency · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.leanTHEOREM composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean
/-- **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 h2The uniqueness of the canonical cost function under the original five conditions is a separate, proved theorem. composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean