Foundation Ontology Predicates

Existence as a selection outcome

In classical logic, existence and truth are primitive notions. Recognition Science replaces them with operational definitions: a thing exists if it is a stable configuration under a cost function, and a proposition is true if it stabilizes under repeated recognition. The ledger, a discrete record of events, defines these predicates and proves their consequences.

The central result is that only one value satisfies the existence predicate. The theorem rs_exists_unique_one proves that the predicate RSExists x is equivalent to x = 1. This means the only stable configuration under the cost function is the value 1, where the defect, the measure of instability, collapses to zero. The framework also proves that the value 0⁺, representing "nothing," is not selectable, since its defect is unbounded.

The framework extends existence to configurations and to a ladder of values. A configuration exists if its ratio to a reference is 1, and a value is real if it is existent and lies in the phi-ladder, the set of powers of the golden ratio. The framework proves that 1 is real, and that the phi-ladder contains 1.

In Recognition Science, the meta-principle "nothing cannot recognize itself" is not an axiom but a derived theorem. The framework proves that the defect of 0⁺ is unbounded, making "nothing" unselectable. This turns a metaphysical claim into a mathematical consequence.

The framework's library, a machine-checked collection of formal theorems, proves these results. The framework establishes that existence is a selection outcome, not a primitive, and that the selection rule forces a unique existent value. This is a concrete step in the framework's program of deriving physical structure from the cost of recognition.

/-- The only RSExistent value is 1. -/
theorem rs_exists_unique_one : ∀ x : ℝ, RSExists x ↔ x = 1 := by
  intro x
  constructor
  · intro ⟨hpos, hdef⟩
    exact (defect_zero_iff_one hpos).mp hdef
  · intro hx
    rw [hx]
    exact ⟨by norm_num, defect_at_one⟩

/-- For any threshold, sufficiently small positive values have defect exceeding it.
    This means "approaching nothing" has unbounded cost. -/
theorem nothing_unbounded_defect :
    ∀ C : ℝ, ∃ ε > 0, ∀ x, 0 < x → x < ε → C < defect x :=
  nothing_cannot_exist

/-- Unity is RSReal (trivially, as φ⁰ · φ⁰ = 1). -/
theorem rs_real_one : RSReal 1 := by
  constructor
  · exact rs_exists_one
  · use 0, 0
    simp [PhiForcing.φ]

theorem one_mem_phi_ladder : (1 : ℝ) ∈ phi_ladder :=
  ⟨0, by simp [PhiForcing.φ]⟩

What this page does not claim

This framework does not prove that the golden ratio is the only self-similar scaling. This framework does not define the cost function J; it assumes it. This framework does not claim that classical logic is wrong, only that RS offers an alternative operational ontology.

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/OntologyPredicates.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: