Embeds
plain-language theorem explainer
Embeds defines the structure of an embedding from any theory T into the universal structure R via a state map together with a reflexivity condition that witnesses structure preservation. Researchers working on the Reality Recognition Framework cite this when constructing the three embeddings required for framework completeness. The declaration is a direct structure definition with no additional proof obligations beyond the reflexivity axiom.
Claim. An embedding of a structure $T$ into the universal structure $R$ consists of a map $embed : T → R.State$ together with the condition that this map preserves structure, witnessed by the reflexivity equation $embed = embed$.
background
UniversalStructure is the single structure that manifests as physics, logic, and experience; it comprises a state space, a recognition relation admitting self-recognition, and a non-negative strain functional. The module states that the final claim is the existence of one such R into which physics, logic, and qualia all embed, with φ-based scaling and ledger closure, so that reality is recognition rather than merely described by it. Upstream results supply concrete maps, including the orbit embedding of LogicNat into the positive reals and the embedding of small-deviation states into complex Hilbert space, that can be lifted to instances of this structure.
proof idea
The declaration is a structure definition. It introduces the embed field and requires structure_preserved to hold by reflexivity, which is immediate from the equality and requires no further lemmas or tactics.
why it matters
This structure supplies the basic embedding mechanism used by the three downstream theorems that establish physics, logic, and qualia each embed into the universal structure, thereby discharging the framework-completeness proposition. The module doc identifies this as the ultimate isomorphism; it directly supports the T0-T8 forcing chain by providing the embedding step that carries the phi-ladder and recognition composition law into the single universal object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.