add_comm
plain-language theorem explainer
Commutativity of addition on the base-neutral finite orbit of repeated distinction: for any two orbit naturals a and b, a + b equals b + a. Anyone building Peano-style arithmetic on DistinctionNat, or lifting it into cost algebra and φ-ring constructions, cites this. The proof is a short induction on a that rewrites with the four zero/succ addition identities and the inductive hypothesis.
Claim. For all orbit naturals $a,b$ (the inductive type of finite distinction orbits with constructors zero and successor), addition is commutative: $a + b = b + a$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with constructors zero and succ, introduced as the primitive counting object of the recognition calculus (K2.12). Addition on it is defined by recursion on the second argument in the usual Peano style, so the four elementary identities a + 0 = a, a + succ b = succ(a + b), 0 + a = a, and succ a + b = succ(a + b) are available as definitional or simp lemmas in this module.
The same commutativity statement already exists upstream for LogicNat (arithmetic extracted from pure logic) and later for PRC integers. Here the goal is the orbit-native copy: addition must be a commutative monoid operation before cancellation, toNat transport, and the rest of OrbitArithmetic can proceed.
Local setting is Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic, which equips DistinctionNat with the first layer of arithmetic without assuming classical Peano axioms as postulates.
proof idea
Induct on a. In the zero case, rewrite with zero_add_eq and add_zero_eq to obtain 0 + b = b + 0. In the successor case, rewrite with succ_add_eq and add_succ_eq, then apply the inductive hypothesis to finish succ n + b = b + succ n. No external library commutativity is invoked; the argument is pure structural induction on the orbit type using the four local addition identities.
why it matters
Commutativity is the first non-definitional algebraic law on DistinctionNat addition. Downstream it is used heavily: CostAlgebra's H_dAlembert (the multiplicative d'Alembert form whose continuous solution is cosh, feeding the Recognition Composition Law and J-cost uniqueness T5), F2Power's additive group instance, PhiRing's integer coefficients a + bφ, Cosmology.RungCoarsen cross-addition, and Cost lemmas such as the quadratic expansion of J near 1. Without a + b = b + a on the orbit naturals, those lifts cannot treat addition as a commutative monoid operation.
In the forcing chain this sits under the primitive recognition calculus that eventually supports T5–T8 (J-uniqueness, φ, eight-tick octave, D = 3). It is scaffolding for arithmetic, not a physics claim by itself, but it is a load-bearing lemma: used_by_count is high across algebra and constants modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.