RSReal_synth
plain-language theorem explainer
RSReal_synth D F x defines a synthesized RS-real by requiring that x satisfies the recognition existence predicate and equals F(u) for some element u drawn from the discrete skeleton D. Researchers parameterizing discrete embeddings or configuration spaces in Recognition Science cite this construction when bridging quantized sets to real values. The definition is a direct conjunction of the two predicates with no auxiliary lemmas.
Claim. Let $D$ be a discrete skeleton in a set $U$ and let $F:U→ℝ$ be a synthesis map. Then $x∈ℝ$ is a synthesized RS-real if $x$ is RS-existent (J-cost vanishes) and $x=F(u)$ for some $u∈D$.
background
Recognition Science treats existence as an outcome of cost minimization under the unique J function. RSExists x holds precisely when J-cost(x)=0, equivalently when defect(x)=0 and x>0. The module defines RSReal as the conjunction of RSExists with discreteness; the present definition replaces the explicit phi-ladder condition with membership in the image of an arbitrary synthesis map F on a discrete skeleton D.
proof idea
The definition is a one-line conjunction of the RSExists predicate with the existential image condition under F. No lemmas are invoked beyond the imported definitions of RSExists.
why it matters
This supplies the parameterized form of RSReal required by Paper Equation 9 for embedding discrete skeletons into the reals. It is used directly by the equivalence RSReal_synth_iff, which reduces the statement to x=1 together with the image condition via the uniqueness result rs_exists_unique_one. In the broader framework it realizes the discrete-to-continuous bridge that supports the phi-ladder and the eight-tick octave once D and F are specialized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.