IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.IntegerDivisibility
Defines integer divisibility (dvdZ) on the balanced-integer model used by Primitive Recognition Calculus, together with the basic lattice facts: reflexivity, transitivity, compatibility with addition, unit and zero laws. Anyone building gcd, primes, or rung arithmetic on the phi-ladder cites this layer. The file is mostly definitional plus short algebraic lemmas over the IntegerOrder and IntegerRational imports.
claimOn the balanced integers of the recognition calculus, write $a \mid_Z b$ when $b = a \cdot k$ for some integer $k$. The relation is reflexive and transitive, stable under addition, satisfies $1 \mid_Z n$ and $n \mid_Z 0$ for all $n$, and is compatible with the balanced-to-ordinary integer embedding.
background
Primitive Recognition Calculus grows classical number structure from recognition primitives rather than assuming $\mathbb{Z}$ as a black box. Upstream modules supply ordered integers and the integer/rational bridge; this file sits in the Grow path and installs divisibility on that carrier.
The balanced integer representation (sign-symmetric encoding used throughout the monolith) comes with maps toInt / reconstruction. Equality lemmas balanced_toInt_eq and balanced_of_toInt_eq pin when two balanced codes denote the same ordinary integer, so divisibility can be stated without representation noise.
dvdZ is the divisibility predicate on that type. The companion facts are the standard preorder and ideal-like properties needed before gcd, primes, or ladder-rung arithmetic can be stated cleanly.
proof idea
Definition module with short algebraic lemmas, not a deep proof development. dvdZ is introduced as existence of a multiplier in the balanced integers. Reflexivity and the unit/zero laws are immediate from the ring operations. Transitivity and additivity unfold the existential witnesses and reassociate products using the IntegerRational and IntegerOrder infrastructure. The balanced/toInt pair of lemmas are representation-coherence facts so later files may switch between codes and ordinary integers freely.
why it matters in Recognition Science
Divisibility is the gate to unique factorization, gcd, and any statement that a recognition rung, tick count, or charge index divides another. In the RS forcing chain, integer structure underwrites the eight-tick octave (period $2^3$), discrete ladder exponents in the mass formula, and integrality constraints on dimensional and counting arguments (T7, T8).
No downstream edges are recorded on this page yet; the natural consumers are later Grow modules (gcd, primes, modular arithmetic) and any foundation lemma that needs $a \mid b$ on recognition integers. Without this thin layer, those developments would re-prove the same preorder facts inline.
scope and limits
- Does not define gcd, lcm, primes, or unique factorization.
- Does not prove Euclidean algorithm or well-foundedness of the divisibility order.
- Does not treat divisibility in the rationals or in modular rings.
- Does not connect dvdZ to physical constants, phi-ladder rungs, or forcing steps T0–T8 by itself.
- Does not record downstream consumers; used_by is empty on this page.