embed_zero
plain-language theorem explainer
The embedding of the identity element of the logic naturals under any generator maps to exactly 1 in the reals. Researchers building arithmetic from the orbit under the Law of Logic cite this as the zero base case. The equality holds immediately by the recursive definition of the embedding function.
Claim. Let $γ$ be a non-trivial positive real generator. The embedding of the identity element of the logic naturals into the positive reals equals $1$.
background
The Generator structure consists of a positive real value distinct from one, guaranteed by the Law of Logic via the non_trivial field. LogicNat is the inductive type whose identity constructor represents the zero-cost element and whose step constructor represents iteration, mirroring the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The embed function maps LogicNat into positive reals by sending identity to 1 and each step to multiplication by the generator value. This declaration sits inside the module that derives arithmetic directly from the functional equation of logic. The upstream embed definition supplies the two recursive clauses that make the identity case immediate.
proof idea
One-line wrapper that applies the base case of the embed definition directly via reflexivity.
why it matters
This base case is invoked inside the proof of embed_add, the multiplicative homomorphism showing that addition on LogicNat corresponds to multiplication of orbit elements. It supplies the zero case required to complete the structural identification of LogicNat with the orbit generated by the Law of Logic. In the Recognition framework it anchors the passage from the functional equation to natural-number arithmetic before further operations and the forcing chain are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.