pith. machine review for the scientific record. sign in
theorem proved term proof high

zero_mul

show as:
view Lean formalization →

Zero multiplied by any element of the logic-forced natural numbers equals zero. Researchers deriving arithmetic directly from the recognition functional equation cite this left-annihilation property as a basic building block. The proof is a one-line induction on the two-constructor structure of LogicNat that applies the successor-multiplication identity followed by the zero-addition reduction.

claimFor every natural number $n$ in the orbit forced by the Law of Logic, $0 · n = 0$.

background

LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator); it encodes the smallest subset of positive reals closed under multiplication by the fixed point γ and containing 1. Multiplication and addition on LogicNat are defined recursively from these constructors, with the successor-multiplication rule and zero-addition identity already established as theorems in the same module. The local setting is the extraction of Peano arithmetic as theorems from the single functional equation of Recognition Science, without external axioms.

proof idea

The proof is a direct induction on n. The identity base case holds by reflexivity. The successor case rewrites via the successor-multiplication theorem, applies the inductive hypothesis, and finishes with the zero-addition theorem.

why it matters in Recognition Science

This theorem supplies the left-zero property required by downstream structures such as PhiInt in the phi-ring and the d'Alembert classification theorems used for cost-function analysis. It forms part of the arithmetic layer that converts the J-uniqueness and Recognition Composition Law into concrete number operations, supporting the forcing chain from logic to the eight-tick octave and spatial dimension count. No open scaffolding remains at this step.

scope and limits

formal statement (Lean)

 183theorem zero_mul (n : LogicNat) : zero * n = zero := by

proof body

Term-mode proof.

 184  induction n with
 185  | identity => rfl
 186  | step n ih =>
 187    show zero * succ n = zero
 188    rw [mul_succ, ih, zero_add]
 189

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.