one_mem_phi_ladder
plain-language theorem explainer
The declaration shows that the real number 1 belongs to the φ-ladder, the discrete set of all powers φ^n for integer n. Researchers working on the Recognition Science ontology cite it when establishing the base case for the unit element as a stable configuration under J-cost. The proof is a direct term construction that supplies the exponent zero and simplifies the power.
Claim. $1$ belongs to the set of all real numbers of the form $φ^n$ for $n ∈ ℤ$, where $φ$ is the golden ratio.
background
The φ-ladder is defined locally as the set {x | ∃ n : ℤ, x = φ^n}, serving as the discrete skeleton for the operational ontology. In this setting RSExists x holds exactly when the defect of x collapses to zero under coercive projection, and RSTrue P holds when P stabilizes under recognition iteration. Upstream results in NucleosynthesisTiers and StillnessGenerative introduce the same ladder as φ^n for tier or integer index, supplying the self-similar scaling that follows from the Recognition Composition Law.
proof idea
The proof is a term-mode construction. It supplies the witness 0 for the existential quantifier in the definition of phi_ladder and applies simplification on φ^0 using the definition of φ from PhiForcing.
why it matters
This membership is applied directly in the downstream theorem RSReal_gen_phi_one, which concludes RSReal_gen phi_ladder 1. It supplies the base case required for the ontology predicates that derive existence from defect zero, consistent with the meta-principle that nothing cannot recognize itself and the forcing chain that selects φ as the self-similar fixed point. The result supports the numeric verification of paper examples in Section 4.1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.