dvdZ_refl
plain-language theorem explainer
Every signed orbit divides itself under the balanced-product divisibility relation. Number theorists working in the primitive recognition calculus cite this as the reflexivity law for integer divisibility on signed orbits. The proof is a short term construction: the witness is the multiplicative unit, and equality of integer images follows from the multiplication and unit lemmas plus omega.
Claim. For every signed orbit $a$ (a difference of two distinction naturals, intended as $\mathrm{pos}-\mathrm{neg}$), $a$ divides $a$: there exists a signed orbit $c$ such that the product $a\cdot c$ is balanced with $a$ (same integer image under the canonical map to $\mathbb{Z}$).
background
Signed orbits are the integer layer of the primitive recognition calculus: a pair of distinction naturals interpreted as a difference $\mathrm{pos}-\mathrm{neg}$, with a canonical map toInt into $\mathbb{Z}$. Multiplication of signed orbits is defined so that it intertwines with ordinary integer multiplication (mul_toInt).
Two signed orbits are balanced when they represent the same integer (equivalently, equal nonnegative parts after normalization). Divisibility dvdZ a b means there exists $c$ with $a\cdot c$ balanced to $b$. The unit signed orbit has integer image $1$ (one_toInt).
This module sits in the Grow layer of Foundation.PrimitiveRecognitionCalculus, building divisibility after IntegerRational and IntegerOrder, before higher arithmetic used by recognition forcing.
proof idea
Instantiate the existential in the divisibility definition with the multiplicative unit. It remains to show that $a\cdot 1$ is balanced with $a$. Apply balanced_of_toInt_eq, reducing to equality of integer images. Rewrite with mul_toInt and one_toInt to obtain $a.\mathrm{toInt}\cdot 1 = a.\mathrm{toInt}$, then close by omega.
why it matters
Reflexivity is the first algebraic law for the integer divisibility predicate on signed orbits. Sibling results in the same file (transitivity, compatibility with addition, $1\mid a$, $a\mid 0$) assemble a preorder and ideal-like structure needed for later rung arithmetic and mass-ladder bookkeeping in Recognition Science.
No downstream consumers are wired yet in the graph; the lemma is infrastructure. It does not itself touch T5–T8, the Recognition Composition Law, or the $\varphi$-ladder, but it underwrites the integer substrate those landmarks eventually use when counting ticks, gaps, and divisibility constraints on orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.