RSReal_synth_iff
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not construct or specify any concrete discrete skeleton D.
- Does not verify that a given map F lands in stable configurations.
- Does not invoke the explicit form of the J-cost function.
- Does not address multiplicity of realizations beyond uniqueness at 1.
formal statement (Lean)
494theorem RSReal_synth_iff {U : Type*} {D : Set U} {F : U → ℝ} {x : ℝ} :
495 RSReal_synth D F x ↔ x = 1 ∧ ∃ u ∈ D, x = F u := by
proof body
Term-mode proof.
496 simp only [RSReal_synth, rs_exists_unique_one]
497
498/-- The φ-ladder as a specific discrete skeleton. -/