RSReal_gen_at_one
plain-language theorem explainer
Unity satisfies the general RSReal predicate for any discrete skeleton D containing it, because RSExists holds at 1 by prior defect computation. Researchers instantiating RSReal for concrete ladders such as the phi-ladder cite this when establishing the base case. The proof is a direct term that pairs the upstream result on RSExistence of unity with the membership hypothesis.
Claim. If $1$ belongs to a subset $D$ of the reals, then $1$ is RSExistent and lies in $D$.
background
The module introduces RSReal with a general discrete skeleton $D$ as the conjunction of RSExists and membership in $D$, where RSExists means the configuration has zero defect under the J-cost. The local theoretical setting treats existence as a selection outcome from cost minimization rather than a primitive. Upstream, the theorem establishing RSExistence at unity follows from direct evaluation of the defect vanishing at that point.
proof idea
The term proof constructs the required conjunction by applying the upstream theorem that unity is RSExistent together with the given hypothesis that 1 lies in D.
why it matters
This result supplies the base case invoked by the downstream theorem placing 1 on the phi-ladder, which supports numeric verification of paper examples in Section 4.1. It anchors the discrete skeleton at unity, the self-similar fixed point arising in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.