Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic

show as:
view Lean formalization →

Orbit positions carry addition defined as concatenation of repetition sequences. The module proves the resulting monoid laws (commutativity, associativity), both-sided cancellation, and compatibility with the natural-number embedding. Anyone citing primitive recognition calculus, orbit divisibility, or signed-orbit growth lemmas needs this layer. Arguments are inductive on the orbit constructors, routed through the toNat homomorphism.

claimOrbit positions form a monoid under addition $+$ given by concatenation of repetition. For positions $a,b,c$: $a+0=a=0+a$, $a+b=b+a$, $(a+b)+c=a+(b+c)$, and left/right cancellation hold. The embedding $\mathrm{toNat}$ is injective and satisfies $\mathrm{toNat}(a+b)=\mathrm{toNat}(a)+\mathrm{toNat}(b)$.

background

In the Primitive Recognition Calculus, an orbit position records a discrete repetition count for a recognition event. The parent Orbit module supplies the inductive type of positions and the map into ordinary natural numbers.

K4.5 treats addition as concatenation of repetition: placing one finite repetition block after another. Zero is the empty block; successor appends one more tick. This monoid is the arithmetic substrate on which later divisibility, kernel, and comparison results are stated.

Notation follows the inductive constructors (zero/succ style) and the embedding into $\mathbb{N}$, so monoid identities can be checked either by direct induction or by transport along the embedding once injectivity is known.

proof idea

Definitional core plus inductive lemmas. Addition is introduced by recursion on constructors (zero and successor clauses for each argument). The basic reduction equations (add-zero, zero-add, add-succ, succ-add) are immediate from that recursion.

Commutativity, associativity, and left/right cancellation are proved by induction on the orbit structure. Compatibility of addition with the natural embedding, together with injectivity of that embedding, lets several identities reduce to the corresponding facts on $\mathbb{N}$. This is a structural arithmetic module, not a one-line wrapper.

why it matters in Recognition Science

This is the K4.5 layer of the foundation: without a coherent monoid on orbit positions, later calculus cannot state growth or divisibility claims. Downstream importers include OrbitDivisibility, Kernel, IntegerRational, and the Grow family of signed-orbit lemmas (zero-le characterizations and right-multiplication inequalities under nonnegativity flags).

Those Grow modules need cancellation and the toNat bridge to move inequalities between the orbit monoid and ordinary arithmetic. IntegerRational and Kernel likewise rely on additive structure when relating orbit counts to integer and rational data. The module therefore sits under every comparison and divisibility result in the primitive recognition stack.

scope and limits

used by (5)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (21)