embed_add
The embedding of LogicNat into positive reals preserves addition as multiplication for any generator γ. Researchers deriving arithmetic from the law of logic cite this when showing that iteration counts act as exponents in the orbit. The proof is by induction on the second argument, reducing the successor case with the recursive definitions of addition and embedding followed by ring simplification.
claimLet γ be a generator and let a, b be elements of the logic-induced naturals. Then the embedding of a + b equals the product of the embeddings of a and b.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step (one iteration), forming the smallest subset of positive reals closed under multiplication by γ.value and containing 1. The embed function is defined recursively: identity maps to 1 and step n maps to γ.value times the embedding of n. Addition on LogicNat satisfies add_zero (n + zero = n) and add_succ (n + succ m = succ (n + m)). A generator is any positive real other than 1, extracted from the non-triviality clause of the law of logic.
proof idea
The proof is by induction on b. The identity case rewrites via add_zero, embed_zero, and mul_one. The step case rewrites via add_succ and embed_succ on both sides, applies the inductive hypothesis, and closes with ring.
why it matters in Recognition Science
This homomorphism shows that LogicNat is precisely the orbit parameterized by iteration count, completing the structural identification of naturals with multiplicative powers. It feeds the arithmetic layer of the foundation module and supports later derivations of the phi-ladder and mass formula. In the T0-T8 chain it supplies the discrete counting structure required before forcing D = 3 and the eight-tick octave.
scope and limits
- Does not prove commutativity or associativity of addition on LogicNat.
- Does not extend the homomorphism to subtraction or division.
- Does not address multiplication defined directly on LogicNat.
- Does not require specific numerical values of γ beyond the generator axioms.
formal statement (Lean)
576theorem embed_add (γ : Generator) (a b : LogicNat) :
577 embed γ (a + b) = embed γ a * embed γ b := by
proof body
Term-mode proof.
578 induction b with
579 | identity =>
580 show embed γ (a + LogicNat.zero) = embed γ a * embed γ LogicNat.zero
581 rw [LogicNat.add_zero, embed_zero, mul_one]
582 | step b ih =>
583 show embed γ (a + LogicNat.succ b) = embed γ a * embed γ (LogicNat.succ b)
584 rw [LogicNat.add_succ, embed_succ, embed_succ, ih]
585 ring
586
587/-- The embedding is the natural-number power of `γ.value`. -/