RSReal_gen
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.