embed_zero
plain-language theorem explainer
The embedding of LogicNat's zero element under any generator γ lands at the multiplicative identity 1 in the reals. Workers constructing the orbit homomorphism from logic naturals to positive reals cite this base case when proving additivity. The proof is immediate reflexivity on the definition of embed at the identity constructor.
Claim. Let $γ$ be a generator. Let $0$ denote the identity constructor of the logic naturals. Then the orbit embedding satisfies $embed(γ, 0) = 1$.
background
Generator is the structure of a positive real value distinct from 1, extracted from the non_trivial witness of SatisfiesLawsOfLogic. LogicNat is the inductive type whose identity constructor represents the zero-cost element and whose step constructor iterates multiplication by the generator value, forming the orbit {1, γ, γ², …}. The embed function is defined by sending identity to 1 and step n to γ.value times the embedding of n.
proof idea
One-line wrapper that applies reflexivity to the clause embed γ LogicNat.identity = 1 inside the definition of embed.
why it matters
Supplies the base case required by the downstream embed_add theorem, which shows that addition on LogicNat corresponds to multiplication on the orbit. This completes the structural identification of LogicNat with the multiplicative orbit forced by the Law of Logic and feeds the derivation of arithmetic inside the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.