RSReal
plain-language theorem explainer
RSReal declares a real x to be RS-real when it satisfies the RS existence predicate and belongs to the discrete subgroup generated by integer powers of the golden ratio phi. Researchers constructing the quantized configuration space cite this predicate to restrict attention to algebraically stable values on the phi-ladder. The definition is assembled as the direct conjunction of RSExists with an existential statement over the phi powers.
Claim. A real number $x$ is RS-real if it satisfies RS existence (i.e., $x>0$ and defect$(x)=0$) and there exist integers $n,m$ such that $x=φ^n φ^m$, where $φ$ is the self-similar fixed point.
background
In the Recognition Science ontology, RSExists asserts that a positive real has vanishing defect under the J-cost function, so the configuration is stable under recognition iteration. RSReal adds the requirement that $x$ lie in the discrete configuration space, modeled here as the subgroup generated by integer powers of phi. The module OntologyPredicates treats existence and truth as selection outcomes of cost minimization rather than primitives, with the local setting given by the selection rule that $x$ exists precisely when defect$(x)$ collapses to zero under coercive projection.
proof idea
The definition is a direct conjunction of the RSExists predicate with the algebraic membership condition that $x$ equals phi to the power n times phi to the power m for some integers n and m. No lemmas or tactics are invoked beyond the referenced definition of RSExists and the phi constant supplied by PhiForcing.
why it matters
RSReal supplies the discrete restriction used by rs_real_one (which verifies unity is RS-real), RSReal_gen (the generalization to arbitrary discrete skeletons), and godel_not_obstruction (which relies on a unique cost minimizer in the configuration space). It realizes the discrete phi-ladder forced in T6-T7 of the unified forcing chain and supports the eight-tick octave structure of T8 by ensuring only algebraically quantized values count as real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.