IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.OrbitDivisibility
Defines divisibility, units, and primality for orbit positions in the primitive recognition calculus. Supplies the multiplicative unit, the divides relation, nontrivial factorizations, and prime orbits on top of orbit arithmetic. Downstream kernel and Euclidean-algorithm modules import this layer. The content is largely definitional with elementary algebraic lemmas (reflexivity, zero, unit laws).
claimOn the multiplicative monoid of orbit positions, introduce the unit $1$, the relation $a \mid b$, units, nontrivial factorizations, and prime orbits, together with the standard facts $1 \neq 0$, $a \mid a$, $a \mid 0$, and the unit laws $a \cdot 1 = a = 1 \cdot a$.
background
Primitive recognition calculus treats discrete orbit positions as the carriers on which recognition cost and forcing later act. The parent module OrbitArithmetic already equips those positions with multiplication and the basic monoid operations.
This module adds the divisibility layer: a distinguished multiplicative unit orbit, the predicate that one orbit divides another, the notion of a unit, nontrivial factorizations, and prime orbits. Sibling names in the module include the unit one, conversion one_toNat, inequalities such as one_ne_zero, the unit laws, associativity, divides, unit, nontrivialFactorization, and primeOrbit, plus elementary closure facts (divides_refl, divides_zero).
The setting is purely algebraic foundation work inside Foundation.PrimitiveRecognitionCalculus; no continuum limits or physical constants appear here.
proof idea
Definition-and-lemma module rather than a single deep theorem. The unit orbit and the divides relation are introduced by definition; unit laws and associativity are recorded as equalities against the ambient monoid structure from OrbitArithmetic. Reflexivity of divides and the fact that everything divides zero are short algebraic arguments. Primality and nontrivial factorization are predicate definitions ready for the Euclidean layer.
why it matters in Recognition Science
Kernel and OrbitEuclidean both import this module, so every later argument that factors orbits, extracts primes, or runs a Euclidean algorithm on recognition orbits depends on these definitions. In the Recognition Science stack this sits under the primitive calculus that eventually supports the forcing chain (T0–T8), where discrete orbit structure and eight-tick periodicity must be well-defined before uniqueness of $J$ and $\varphi$ are forced. Without a clean divisibility layer, prime-orbit uniqueness and gcd-style arguments cannot be stated.
scope and limits
- Does not prove unique factorization or existence of gcds; only defines divides and primes.
- Does not connect orbit primes to physical mass rungs or the phi-ladder.
- Does not establish the eight-tick octave or T7 periodicity.
- Does not mention J-cost, RCL, or continuum recognition functionals.
- Does not discharge any sorry; it is infrastructure, not a forcing theorem.
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