Encyclopedia Foundation Foundation Cost Axioms Unity Is Unique Existent

ARTICLE 3 claims 3 theorems

Foundation Cost Axioms Unity Is Unique Existent

In Recognition Science, a number exists only when it sits at ratio one to itself, and that point is unique.

Verify this page

The unity criterion

In the Recognition Science framework, the statement unity_is_unique_existent is a proved theorem about the framework's own definition of existence. The framework defines a positive number x as existing when a certain cost function J(x) equals zero. The theorem proves that this happens if and only if x = 1. In plainer terms: among all positive numbers, exactly one number satisfies the framework's existence criterion, and that number is unity.

The cost function in question is J(x) = ½(x + 1/x) − 1. It measures the cost of being at ratio x relative to unity, where unity itself costs nothing: J(1) = 0. The theorem J_eq_zero_iff proves that for any positive x, J(x) = 0 holds exactly when x = 1. The full theorem unity_is_unique_existent extends this to all real x, including non-positive values, where the existence definition's positivity requirement makes the statement vacuously false except at x = 1.

The framework derives this cost function from three primitive axioms: normalization (F(1) = 0), a composition law F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y), and calibration (second log-derivative at zero equals 1). A separate uniqueness theorem, proved under additional regularity hypotheses, shows that any function satisfying these axioms plus continuity and convexity must equal J. The existence criterion then follows as a theorem, not an assumption.

What the theorem does not claim: it does not assert that only the number 1 exists in any ordinary sense. It establishes a formal equivalence within the framework's own definition of existence. It does not prove that the cost function J is the only possible cost function without the regularity hypotheses; the uniqueness theorem requires continuity and convexity conditions. The theorem also does not address what it means for physical objects to exist; it concerns a formal definition in a mathematical framework.

The consequence of this theorem is that the framework's notion of existence is internally consistent: the criterion picks out exactly one point. This uniqueness is what allows the framework to proceed to derive further structure, such as the golden ratio as a self-similar scaling, from a well-defined foundation.

THEOREM J_eq_zero_iff · IndisputableMonolith/Foundation/CostAxioms.lean
J_eq_zero_iff · IndisputableMonolith/Foundation/CostAxioms.lean:151 
/-- J equals zero exactly at x = 1. -/
theorem J_eq_zero_iff {x : ℝ} (hx : 0 < x) : J x = 0 ↔ x = 1 := by
  constructor
  · intro hJ
    simp only [J] at hJ
    -- (x + 1/x)/2 - 1 = 0  ⟹  x + 1/x = 2  ⟹  x² - 2x + 1 = 0  ⟹  x = 1
    have h1 : x + x⁻¹ = 2 := by linarith
    have hx0 : x ≠ 0 := hx.ne'
    have h2 : x^2 + 1 = 2 * x := by
      field_simp at h1
      linarith
    have h3 : (x - 1)^2 = 0 := by ring_nf; linarith
    have h4 : x - 1 = 0 := by nlinarith [sq_nonneg (x - 1)]
    linarith
  · intro hx1
    simp [J, hx1]
THEOREM unity_is_unique_existent · IndisputableMonolith/Foundation/CostAxioms.lean
unity_is_unique_existent · IndisputableMonolith/Foundation/CostAxioms.lean:235 
/-- Unity is the unique existent. -/
theorem unity_is_unique_existent : ∀ x : ℝ, Exists x ↔ x = 1 := by
  intro x
  by_cases hx : 0 < x
  · exact law_of_existence hx
  · simp only [Exists]
    constructor
    · intro ⟨hpos, _⟩; exact absurd hpos hx
    · intro heq; subst heq; exact ⟨one_pos, by simp [J]⟩
THEOREM uniqueness_specification · IndisputableMonolith/Foundation/CostAxioms.lean
uniqueness_specification · IndisputableMonolith/Foundation/CostAxioms.lean:317 
/-- **T5 Uniqueness (Specification)**:
    Any function F satisfying the three cost axioms with regularity equals J.

    This is the central uniqueness theorem of Recognition Science.
    The complete proof is in CostUniqueness.lean via T5_uniqueness_complete.

    The proof structure is:
    1. CostFunctionalAxioms.composition gives d'Alembert: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)
    2. Substituting G(t) = F(exp(t)) transforms to cosh-additive: G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t)
    3. Shifting H = G + 1 gives standard d'Alembert: H(s+t) + H(s-t) = 2H(s)H(t)
    4. The unique continuous solution is H(t) = cosh(t), so G(t) = cosh(t) - 1
    5. Therefore F(x) = cosh(log(x)) - 1 = ½(x + x⁻¹) - 1 = J(x)

    The regularity hypotheses (Aczél theory for d'Alembert equations) are stated
    explicitly. These are standard results from functional equation theory:
    - Continuous d'Alembert solutions are smooth (Aczél 1966)
    - Smooth d'Alembert solutions satisfy ODE H'' = H
    - Linear ODE regularity bootstrap

    See `IndisputableMonolith.T5_uniqueness_complete` for the rigorous proof. -/
theorem uniqueness_specification (F : ℝ → ℝ) [CostFunctionalAxioms F]
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hConvex : StrictConvexOn ℝ (Set.Ioi 0) F)
    -- Regularity hypotheses from Aczél's theorem on d'Alembert equations
    (h_smooth : Cost.FunctionalEquation.dAlembert_continuous_implies_smooth_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_ode : Cost.FunctionalEquation.dAlembert_to_ODE_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_cont : Cost.FunctionalEquation.ode_regularity_continuous_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_diff : Cost.FunctionalEquation.ode_regularity_differentiable_hypothesis
        (Cost.FunctionalEquation.H F))
    (h_boot : Cost.FunctionalEquation.ode_linear_regularity_bootstrap_hypothesis
        (Cost.FunctionalEquation.H F)) :
    ∀ x, 0 < x → F x = J x := by
  intro x hx
  -- Bridge from CostFunctionalAxioms to T5_uniqueness_complete hypotheses
  -- 1. Symmetry: F(x) = F(1/x)
  have hSymm : ∀ {x : ℝ}, 0 < x → F x = F x⁻¹ :=
    Composition_Normalization_implies_symmetry F
  -- 2. Unit normalization: F(1) = 0
  have hUnit : F 1 = 0 := Normalization.unit_zero
  -- 3. Calibration: deriv (deriv (F ∘ exp)) 0 = 1
  have hCalib : deriv (deriv (F ∘ exp)) 0 = 1 := Calibration.second_deriv_at_zero
  -- 4. CoshAddIdentity: from Composition axiom
  have hCoshAdd : Cost.FunctionalEquation.CoshAddIdentity F :=
    Composition_implies_CoshAddIdentity F
  -- Apply T5_uniqueness_complete with all hypotheses
  unfold J
  exact CostUniqueness.T5_uniqueness_complete F hSymm hUnit hConvex hCalib hCont hCoshAdd
    h_smooth h_ode h_cont h_diff h_boot hx

What this page does not claim

The theorem does not assert that only the number 1 exists in any ordinary sense. The theorem does not prove that J is the only possible cost function without the regularity hypotheses. The theorem does not address what it means for physical objects to exist.

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