RSReal_gen
RSReal_gen provides a generalized predicate for RS-real numbers over an arbitrary discrete skeleton set D. Researchers extending the Recognition Science ontology to different configuration spaces would cite this definition. It is realized as the conjunction of the recognition existence condition and set membership in D.
claimFor a discrete skeleton $Dsubseteqmathbb{R}$ and a real number $x$, $x$ satisfies the generalized RS-real condition if it meets the recognition existence criterion and belongs to $D$.
background
The module establishes an operational ontology where existence is determined by cost minimization under the J function. A number x satisfies the recognition existence condition when it is positive and its defect vanishes, equivalent to J-cost being zero. The standard RS-real predicate further requires x to be of the form phi to integer powers, modeling discreteness via the phi-ladder.
proof idea
This definition is a one-line wrapper that directly conjoins the recognition existence predicate with membership in the set D.
why it matters in Recognition Science
The definition underpins downstream results such as the theorem establishing that 1 satisfies the predicate whenever it lies in D, and the equivalence theorem reducing it to x equals 1 and membership in D. It corresponds to Paper Equation 8 and supports the framework's forcing chain by enabling varied discretizations consistent with J-uniqueness. It touches the open question of how different skeletons relate to the eight-tick octave.
scope and limits
- Does not impose phi-ladder structure on D.
- Does not establish existence or uniqueness of elements satisfying the predicate.
- Does not link to the recognition truth predicate for propositions.
- Does not incorporate measurement maps or native units directly.
Lean usage
theorem RSReal_gen_at_one {D : Set ℝ} (hD : (1 : ℝ) ∈ D) : RSReal_gen D 1 := ⟨rs_exists_one, hD⟩formal statement (Lean)
480def RSReal_gen (D : Set ℝ) (x : ℝ) : Prop :=
proof body
Definition body.
481 RSExists x ∧ x ∈ D
482
483/-- RSReal with synthesis map F : U → ℝ and discrete skeleton D ⊆ U. (Paper Eq. 9) -/