embed_zero
The orbit embedding sends the identity constructor of the logic-forced naturals to the multiplicative identity 1 in the positive reals for any generator. Foundation researchers building arithmetic from the Law of Logic cite this when establishing the base case of the multiplicative homomorphism for the orbit. The proof reduces immediately to the defining clause of the embedding function via reflexivity.
claimLet $γ$ be a non-trivial generator. Then the orbit embedding of the identity element of the logic-forced naturals satisfies $embed(γ, 0) = 1$, where $0$ denotes the identity constructor.
background
The module constructs natural-number arithmetic from the Law of Logic. LogicNat is the inductive type whose identity constructor represents the zero-cost multiplicative identity and whose step constructor iterates multiplication by the generator; this mirrors the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The embed function is defined by sending the identity constructor to 1 and the step constructor n to γ.value times the embedding of n. A Generator is any positive real value ≠ 1, whose existence follows from the non_trivial field of SatisfiesLawsOfLogic.
proof idea
One-line wrapper that applies reflexivity to the defining equation of the embed function at the identity constructor.
why it matters in Recognition Science
This base case is invoked directly by the proof of embed_add, which shows that the embedding is a multiplicative homomorphism: embed γ (a + b) = embed γ a * embed γ b. It supplies the zero case required to derive Peano arithmetic from the functional equation inside the Recognition Science framework.
scope and limits
- Does not address the embedding of any successor or step elements.
- Does not prove existence of generators.
- Does not extend the result to real-valued or complex embeddings.
- Does not interact with the separate embedding defined in HamiltonianEmergence.
formal statement (Lean)
560@[simp] theorem embed_zero (γ : Generator) : embed γ LogicNat.zero = 1 := rfl
proof body
561