IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility
Defines divisibility on orbit positions in the primitive recognition calculus: the multiplicative unit, the divides predicate, units, nontrivial factorizations, and prime orbits. Downstream Kernel and OrbitEuclidean import it for monoid arithmetic. Content is elementary monoid lemmas plus the prime/factorization vocabulary built on OrbitArithmetic.
claimOn the multiplicative monoid of orbit positions, introduce the unit $1$, the relation $a \mid b$, the notion of unit, nontrivial factorization, and prime orbit, together with the basic identities $a \cdot 1 = a = 1 \cdot a$, associativity, reflexivity of divides, and $a \mid 0$.
background
Primitive Recognition Calculus treats discrete orbit positions as the carriers on which recognition cost and forcing later act. The parent module OrbitArithmetic supplies the multiplicative structure; this module equips that monoid with classical divisibility language.
The multiplicative unit orbit position is the identity element $1$ of the monoid. From it one defines $a \mid b$ in the usual way (existence of a cofactor), units (divisors of $1$), nontrivial factorizations, and prime orbits (orbits whose only factorizations are units times associates).
Sibling lemmas record the monoid laws for $1$, reflexivity of divides, and the zero case, so later Euclidean and kernel arguments can quote standard number-theoretic phrasing without re-proving monoid trivia.
proof idea
Definition-and-lemma module, not a single theorem. It introduces one, divides, unit, nontrivialFactorization, and primeOrbit, then proves the elementary monoid identities (unit laws, associativity) and the first divisibility facts (reflexivity, divides zero) by direct unfolding of the OrbitArithmetic operations. No deep forcing or analytic argument appears here.
why it matters in Recognition Science
Supplies the divisibility vocabulary that Kernel and OrbitEuclidean import. Without a clean prime/factorization layer on orbits, Euclidean-style arguments and kernel constructions in the primitive calculus cannot be stated in standard monoid language. In the broader Recognition foundation this sits under the pre-forcing arithmetic scaffolding that later feeds the T0–T8 chain; it does not itself force $\varphi$, the eight-tick octave, or $D=3$.
scope and limits
- Does not prove uniqueness of factorization or a full Euclidean algorithm.
- Does not connect primes to J-cost, RCL, or the forcing chain T5–T8.
- Does not define addition, gcd as an algorithm, or ideal theory.
- Does not claim physical mass, alpha, or dimensional consequences.
used by (2)
depends on (1)
declarations in this module (31)
-
def
one -
theorem
one_toNat -
theorem
one_ne_zero -
theorem
mul_one_eq -
theorem
one_mul_eq -
theorem
mul_assoc -
def
divides -
def
unit -
def
nontrivialFactorization -
def
primeOrbit -
theorem
divides_refl -
theorem
divides_zero -
theorem
one_divides -
theorem
divides_trans -
theorem
divides_mul_right -
theorem
divides_mul_left -
theorem
zero_divides_iff_eq_zero -
theorem
divides_iff_toNat_dvd -
theorem
unit_iff_toNat_eq_one -
theorem
divides_one_iff_unit -
theorem
unit_of_divides_unit -
theorem
divides_antisymm -
theorem
ofNat_ne_zero_of_ne_zero -
theorem
not_unit_ofNat_of_ne_one -
theorem
nontrivialFactorization_iff_toNat -
theorem
primeOrbit_iff_toNat_no_nontrivial_factor -
theorem
unit_or_unit_of_mul_eq_prime -
theorem
primeOrbit_of_unit_or_unit -
theorem
unit_or_eq_of_divides_prime -
structure
OrbitDivisibilityCertificate -
theorem
orbit_divisibility_certificate