embed_succ
plain-language theorem explainer
The embedding of the successor of a logic natural n under generator γ multiplies the orbit value by γ.value. Researchers deriving arithmetic from the Law of Logic cite this as the recursive clause that lets the orbit map respect the successor operation. The equality holds by direct matching of the embed recursive clause to the succ constructor definition.
Claim. Let γ be a non-trivial positive real generator and n an element of the logic naturals. Then the orbit embedding of the successor of n satisfies embed(γ, succ(n)) = γ.value ⋅ embed(γ, n).
background
LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} inside the positive reals; identity stands for the zero-cost element and step for one further multiplication by the generator. The embed function is defined by sending identity to 1 and each step n to γ.value times the embedding of n. A Generator is any positive real other than 1, whose existence is supplied by the non_trivial witness in SatisfiesLawsOfLogic.
proof idea
One-line term proof by reflexivity. The definition of succ n expands to .step n, and the second clause of embed γ on .step n is exactly γ.value * embed γ n, so rfl closes the goal.
why it matters
This supplies the successor case required by the downstream embed_add theorem, which proves that embed is a multiplicative homomorphism and therefore that LogicNat addition corresponds to orbit multiplication. The step completes the translation of Peano structure into the functional equation setting of Recognition Science, directly supporting the derivation of arithmetic from the Law of Logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.