pith. sign in
theorem

embed_add

proved
show as:
module
IndisputableMonolith.Foundation.ArithmeticFromLogic
domain
Foundation
line
576 · github
papers citing
61 papers (below)

plain-language theorem explainer

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.

Claim. Let γ 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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 61)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.