pith. machine review for the scientific record. sign in
def definition def or abbrev high

mul

show as:
view Lean formalization →

Multiplication on LogicNat is defined by recursion on the second argument, returning zero when the second factor is the identity element and otherwise adding the first factor to the product of the first factor with the predecessor. Algebraists building the phi-ring and cost structures cite this when assembling the arithmetic layer of Recognition Science. The definition is a direct recursive unfolding that mirrors the standard Peano construction for natural-number multiplication.

claimLet $N_L$ be the inductive type with constructors identity (zero-cost element) and step. Multiplication $N_L times N_L to N_L$ satisfies $n times identity = 0$ and $n times (step m) = (n times m) + n$, where $0$ and $+$ are the zero and addition already defined on $N_L$.

background

LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, gamma, gamma^2, ...} as the smallest subset of positive reals closed under multiplication by gamma and containing 1; identity is the zero-cost multiplicative identity. The module ArithmeticFromLogic constructs the natural-number operations directly from the Law of Logic, using the same recursive pattern already introduced for addition in the sibling definitions. Upstream, the step constructor of LogicNat is the generator that forces the successor relation, while the mul definitions in IntegersFromLogic and RationalsFromLogic lift this operation to the quotient types.

proof idea

The declaration is a direct recursive definition by pattern matching on the second argument: the identity case returns the zero element already defined in the module, and the step case invokes the sibling addition operation on the recursive call.

why it matters in Recognition Science

This multiplication supplies the ring multiplication used by PhiRing.PhiInt, RecognitionCategory.PhiRingHom, and CostAlgebra.shiftedCompose_val, thereby enabling the coherence-cost calculation J_at_phi and the canonical object of the Recognition Category. It completes the arithmetic scaffolding required for the Recognition Composition Law and the forcing chain that reaches D = 3 spatial dimensions. The definition is cited in every downstream construction that treats LogicNat as a semiring.

scope and limits

Lean usage

theorem mul_identity (n : LogicNat) : n * LogicNat.identity = LogicNat.zero := rfl

formal statement (Lean)

 171def mul : LogicNat → LogicNat → LogicNat
 172  | _, .identity => zero
 173  | n, .step m   => mul n m + n
 174
 175instance : Mul LogicNat := ⟨mul⟩

proof body

Definition body.

 176

used by (40)

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

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.