Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitArithmetic

show as:
view Lean formalization →

Defines addition of orbit positions as concatenation of repetition counts, equipping the primitive orbit type with a commutative monoid structure. Anyone building integer or rational structure on recognition orbits cites this layer. The development is by structural recursion on the successor presentation, with cancellation and injectivity of the natural embedding proved from the recursive clauses.

claimOn orbit positions (repetition counts of a primitive recognition cycle), addition $m + n$ is the concatenation of $m$ and $n$ repetitions. The operation satisfies $0 + n = n = n + 0$, successor recursion, commutativity, associativity, left and right cancellation, and the embedding into $\mathbb{N}$ is injective and preserves addition.

background

Primitive Recognition Calculus treats an orbit as a pure repetition count of a base recognition tick, before signed or rational structure is imposed. The upstream Orbit module supplies that bare position type and its successor/zero presentation; this module adds the binary operation that turns positions into an arithmetic monoid.

Addition is interpreted as concatenation of repetition: placing one block of repetitions after another. The natural-number embedding toNat is the bridge that lets later modules compare orbit arithmetic with ordinary $\mathbb{N}$. Sibling lemmas record the recursive clauses (zero and successor on each side), the monoid laws, cancellation, and injectivity of that embedding.

The local setting is the K4.5 step of the foundation stack: once positions can be added, one can define multiples, divisibility, and the kernel of the recognition map without leaving the orbit language.

proof idea

Definition module with a recursive definition of addition on the zero/successor presentation of orbit positions, plus a short library of monoid and cancellation lemmas. Recursive clauses fix zero and successor on each argument; commutativity and associativity are proved by induction on those clauses. The natural embedding is shown to preserve addition, then injectivity and left/right cancellation follow from the corresponding facts on $\mathbb{N}$ transported along that embedding.

why it matters in Recognition Science

Feeds five downstream modules: the two Grow signed-orbit comparison developments (nonnegativity and right-multiplication inequalities), IntegerRational (integer and rational structure on orbits), Kernel (recognition kernel), and OrbitDivisibility. Without concatenation-as-addition, those layers cannot state multiples, ordered comparisons, or divisibility inside the orbit type. In the broader Recognition stack this is the arithmetic substrate beneath later forcing and mass-ladder constructions that need well-behaved position arithmetic before $\phi$-scaling and eight-tick structure appear.

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)