Encyclopedia Foundation Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness
ARTICLE 3 claims 3 theorems
Foundation Primitive Recognition Calculus Prcnative Cost Uniqueness
A single cost function for recognition events is forced by five plain conditions, and the proof is checked by a machine.
The cost uniqueness result
The cost of a recognition event is the price a system pays for registering a difference. In Recognition Science, this cost is not chosen freely. The framework's central theorem states that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The composition law says the cost of doing two recognitions in sequence is determined by the costs of the individual steps, not by the order in which they are done.
The uniqueness result is proved in a machine-checked library of formal theorems. The proof is axiom-clean: it uses only the three standard axioms of the underlying type theory, with no framework-specific assumptions. This means the result does not depend on any unstated premise about how recognition works. It is a theorem about cost functions in general, and the framework's cost function is the unique solution to the stated conditions.
The library also shows what happens when one of the five conditions is dropped. Without the calibration condition, the composition law alone does not force the cost function. There exist continuous, reciprocal, normalized functions that satisfy the composition law but are not equal to J. This is a sharp boundary: the uniqueness result is exactly as strong as its assumptions, and no stronger.
In Recognition Science, the cost function J is the starting point. From it, the framework derives the golden ratio as the unique self-similar scaling, an eight-tick recognition cycle, and three spatial dimensions. These are later theorems in the forcing chain. The cost uniqueness result is the first link in that chain, and it is the link that makes the rest possible.
The practical consequence is that the framework's predictions do not depend on a choice of cost function. There is only one cost function that satisfies the framework's conditions, so any system that obeys those conditions must use the same cost. This is what makes the framework's later derivations, such as the value of the fine-structure constant, meaningful: they are not fitted to a free parameter, but follow from a forced structure.
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
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
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 uniqueness result does not by itself derive the fine-structure constant or any other physical constant. The proof does not show that the five conditions are the only possible ones; it shows that any cost function satisfying them must be J. The theorem does not claim that the cost function is unique without the continuity condition.
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 exactly is the calibration condition, and why is it necessary for uniqueness?
- How does the composition law relate to the order of recognition events?
- What are the five conditions in full formal detail?
- How does the cost function J lead to the golden ratio and the eight-tick cycle?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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 h2Any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. composition_law_without_calibration_does_not_force_jcost · 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 proof is axiom-clean: it uses only the three standard axioms of the underlying type theory, with no framework-specific assumptions. composition_law_without_calibration_does_not_force_jcost · 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 h2Without the calibration condition, the composition law alone does not force the cost function. composition_law_without_calibration_does_not_force_jcost · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCNativeCostUniqueness.lean