RSReal_synth_iff
plain-language theorem explainer
The equivalence states that a synthesized RS-real value holds exactly when the number is 1 and arises as the image of some element from the discrete skeleton under the synthesis map. Researchers constructing explicit models of stable reals from finite skeletons in Recognition Science cite this result when bridging discrete ontology to continuum quantities. The proof is a one-line simplification that unfolds the synthesized predicate and substitutes the uniqueness of RSExistent values.
Claim. For a discrete skeleton $D$ and synthesis map $F:U→ℝ$, the predicate that $x$ is a synthesized RS-real holds if and only if $x=1$ and there exists $u∈D$ such that $x=F(u)$.
background
In the RS ontology, RSExists asserts that a real number forms a stable configuration under the J-cost function, with defect collapsing to zero. The synthesized variant augments this stability condition with a discrete skeleton $D⊆U$ and map $F$, requiring that the value also equals $F(u)$ for some $u$ in $D$. The module treats existence and truth as selection outcomes from cost minimization rather than primitive notions, with the meta-principle derived as a consequence of the cost structure.
proof idea
The proof is a one-line wrapper that applies simp to unfold the definition of the synthesized RS-real predicate and substitute the uniqueness theorem for RSExistent values.
why it matters
This equivalence supports explicit construction of RS-real numbers from discrete skeletons as described in paper equation 9. It aligns synthesized values with the unique stable point at 1 from the forcing chain and the operational ontology. No downstream applications are recorded, leaving open its role in continuum bridges or lepton derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.