rs_real_one
plain-language theorem explainer
Unity satisfies the RSReal predicate, confirming that 1 is both stable under J-cost minimization and algebraically quantized as a product of integer powers of phi. Researchers deriving the operational ontology of Recognition Science cite this as the base case for discrete stable configurations. The proof is a term-mode construction that splits the conjunction in the RSReal definition and supplies an explicit algebraic witness.
Claim. $1$ satisfies RSReal, i.e., RSExists($1$) holds and there exist integers $n,m$ such that $1 = phi^n · phi^m$.
background
In the OntologyPredicates module, RSReal(x) is defined as the conjunction of RSExists(x) (stable under the J-cost functional with defect collapsing to zero) and discreteness expressed as algebraic membership in the phi-ladder: x equals phi^n times phi^m for integers n and m. The module derives existence and truth as selection outcomes under cost minimization rather than primitive assumptions, with the selection rule that x exists precisely when defect(x) reaches zero under coercive projection. Upstream, rs_exists_one establishes that RSExists(1) holds by norm_num together with defect_at_one, while the defect functional is identified with J for positive arguments.
proof idea
The term proof applies the constructor tactic to the conjunction in the RSReal definition. The first conjunct is discharged by exact application of the upstream theorem rs_exists_one. The second conjunct is witnessed by the pair of integers 0 and 0, with the equality 1 = phi^0 · phi^0 reduced by simp on the PhiForcing.phi definition.
why it matters
This result anchors the RS ontology by confirming the unit element as the unique stable discrete configuration, directly supporting downstream uniqueness theorems such as rs_exists_unique_one and the derivation of the meta-principle as a cost theorem (defect at 0^+ is unbounded, so nothing is not selectable). It instantiates the framework landmark that phi is the self-similar fixed point (T6) and supplies the base case for the phi-ladder mass formula and eight-tick octave structure. No open scaffolding remains here; the declaration closes the trivial case for the selection rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.