Foundation Primitive Recognition Calculus Orbit Arithmetic Mul Zero Eq

The zero rule

In ordinary arithmetic, multiplying any number by zero gives zero. The declaration mul_zero_eq is the Recognition Science library's version of that fact, proved for its own counting system. The system works with a ledger, a discrete record of events, where positions are built from a starting point and a successor step. The proof states that for any position a, the product a * zero equals zero, and it is established by definition: the rule that defines multiplication sends any first argument paired with zero to zero.

The declaration is part of a larger structure called the δ-orbit, which models repeated distinction as arithmetic. Addition is concatenation of repetition, and multiplication is nested repetition. The zero rule is the base case that makes this multiplication behave like the familiar one. The library also proves the companion fact that zero times any position is zero, and that a product of two nonzero positions is nonzero, so the arithmetic has no zero divisors.

What the declaration does not claim is any physical content. It does not say that the ledger is the universe, or that recognition events are literally numbers. It is a formal theorem about an abstract structure, checked by a machine. The proof is a definitional equality, which means it holds by the way multiplication is defined, not by a deeper argument. It is a building block, not a discovery about nature.

The practical consequence is that the framework's arithmetic is sound at its base. If the zero rule failed, everything built on it would be suspect. Its proof, along with the proofs of commutativity and associativity, gives the ledger a solid foundation for the later steps that derive constants and dimensions. The reader can trust that the counting system behaves as expected, at least at this level.

theorem mul_zero_eq (a : DistinctionNat) :
    a * zero = zero := rfl

theorem mul_zero_eq (a : DistinctionNat) :
    a * zero = zero := rfl

theorem zero_mul_eq (a : DistinctionNat) :
    zero * a = zero := by
  induction a with
  | zero => rfl
  | succ n ih =>
      show zero * n + zero = zero
      rw [add_zero_eq, ih]

/-- K4.7. Product of nonzero orbit positions is nonzero. -/
theorem mul_ne_zero {a b : DistinctionNat}
    (ha : a ≠ zero) (hb : b ≠ zero) :
    a * b ≠ zero := by
  intro h
  have hnat : (a * b).toNat = zero.toNat := by rw [h]
  rw [toNat_mul, toNat_zero] at hnat
  rcases Nat.mul_eq_zero.mp hnat with hzero | hzero
  · have : a = zero := by
      apply toNat_inj
      rw [toNat_zero]
      exact hzero
    exact ha this
  · have : b = zero := by
      apply toNat_inj
      rw [toNat_zero]
      exact hzero
    exact hb this

What this page does not claim

The declaration does not claim any physical interpretation for the ledger. The declaration does not claim that multiplication is commutative; that is a separate theorem. The declaration does not claim that the zero rule is derived from deeper principles; it is a definitional equality.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/OrbitArithmetic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: