mul_succ
Multiplication on LogicNat satisfies the successor recursion rule that n times the successor of m equals n times m plus n. Researchers reconstructing arithmetic from the Law of Logic functional equation cite this when establishing the ring structure on the orbit. The proof is immediate from the recursive definition of multiplication via reflexivity.
claimFor all elements $n, m$ in the natural numbers derived from the Law of Logic, $n$ times the successor of $m$ equals $n$ times $m$ plus $n$.
background
LogicNat is the inductive type with an identity constructor for the zero-cost multiplicative identity and a step constructor for one more iteration of the generator; its structure mirrors the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The successor operation applies one step to any LogicNat element. This theorem belongs to the module deriving arithmetic directly from the Law of Logic as a functional equation, without positing Peano axioms.
proof idea
The proof is a one-line wrapper that applies the recursive definition of multiplication on LogicNat, reducing both sides by reflexivity.
why it matters in Recognition Science
This result supplies the successor recursion needed to build the full ring operations on LogicNat. It feeds mul_add for distributivity, mul_one and one_mul for the unit, zero_mul, and the recovery theorem toNat_mul that equates LogicNat multiplication with ordinary Nat multiplication. In the Recognition framework it forms part of the arithmetic layer that supports the forcing chain from the functional equation to integer structure.
scope and limits
- Does not establish commutativity or associativity of multiplication.
- Does not extend the operation to real numbers or continuous structures.
- Does not incorporate J-cost, defect distance, or the phi-ladder.
- Does not address the Recognition Composition Law or the eight-tick octave.
formal statement (Lean)
181@[simp] theorem mul_succ (n m : LogicNat) : n * succ m = n * m + n := rfl
proof body
182