Affine words and typed local quotient coordinates

Abstract

Finite positive words realize gcd-restricted affine actions; computed local quotient coordinates preserve every affine depth response.

Theorem 1.1 (Every mixed word retains an affine form).

$$\forall H\in \mathbb{N},\forall A\in \mathrm{List}({\mathbb{N}}_{>0}),\forall w\in \mathrm{List}(\mathrm{Operation}(A)),\exists a,t\in \mathbb{N},0<a\wedge \mathrm{libraryGcd}(H,A)\mid t\wedge \forall x\in {\mathbb{N}}_{>0},(\mathrm{runWord}(\mathrm{update}(A),w,x)).val=ax+t$$

Proof. Machine-checked in Lean as D5/S3/Factorization/PrimePowers/AffineGcdBehavior.affine_word_translation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be a finite list of positive addends. The named libraryGcd(H,A) is the fold of natural gcd through A, starting at H; in particular an empty list has libraryGcd(H,[]) equal to H. Operation(A) is the sum of positive multipliers and indices in A. Its update multiplies or adds the indexed positive value, and runWord evaluates a list of these operations from left to right on a positive source.

The quantifier over words includes the empty list and imposes no common length bound. The slope is a positive natural number. Every addition contributes a multiple of the library gcd, and subsequent positive multiplications preserve that divisibility.

Theorem 1.2 (Every permitted affine residue has an original-library word).

$$\forall H\in \mathbb{N},\forall A\in \mathrm{List}({\mathbb{N}}_{>0}),\forall a\in {\mathbb{N}}_{>0},\forall t\in \mathbb{N},(2\le H\wedge \mathrm{libraryGcd}(H,A)\mid t)\Rightarrow \exists ws\in \mathrm{List}(\mathrm{Fin}(\mathrm{length}(A))),\forall x\in {\mathbb{N}}_{>0},\mathrm{residue}(H,(\mathrm{runWord}(\mathrm{update}(A),List.cons(Sum.inl(a),List.map(Sum.inr,ws)),x)).val)=\mathrm{residue}(H,ax+t)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/PrimePowers/AffineGcdBehavior.affine_action_realization (✓ std3). ∎

Source. Repository-derived.

Commentary.

For H at least two, every positive slope a and every natural translation t divisible by libraryGcd(H,A) is realized modulo H. The witnessing word first multiplies by a, then executes a finite list of indexed additions from A. A is allowed to be empty; the list of additions and its length are not constrained in advance.

Bézout’s identity places the gcd residue in the additive subgroup generated by the library. In the finite group ZMod(H), the positive addition closure has the same carrier. Closure induction extracts one concrete list of original additions, valid for every positive source x.

Theorem 1.3 (The local code is exactly the affine response quotient).

$$\forall p\in \mathbb{N},\forall h\in \mathbb{N},\forall e\in \mathbb{N},(\mathrm{Prime}(p)\wedge 1\le h\wedge e\le h)\Rightarrow ((\forall X\in \mathbb{Z},\forall Y\in \mathbb{Z},(\mathrm{localEncoding}(p,h,e,\mathrm{residue}(p^h,X))=\mathrm{localEncoding}(p,h,e,\mathrm{residue}(p^h,Y)))\iff (\forall a\in {\mathbb{N}}_{>0},\forall b\in \mathbb{Z},\mathrm{depth}(p,h,0,\mathrm{residue}(p^h,a\times X+p^e\times b))=\mathrm{depth}(p,h,0,\mathrm{residue}(p^h,a\times Y+p^e\times b))))\wedge (\forall c\in \mathrm{LocalCode}(p,h,e),\exists X\in \mathbb{Z},\mathrm{localEncoding}(p,h,e,\mathrm{residue}(p^h,X))=c))$$

Proof. Machine-checked in Lean as D5/S3/Factorization/PrimePowers/AffineGcdBehavior.local_encoding_complete (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every signed pair of sources, equality of the computed tagged local codes is equivalent to equality of every response depth under every positive multiplier and every signed p^e translation. The reverse implication uses the frozen affine classifier after matching signed depth and quotient coordinates to the typed code.

Every LocalCode is represented by an integer source. The construction uses an exact p^e multiple for deep tags, and a p^r times a unit representative for low tags; when M is one the unique unit class is handled directly. Zero and saturation are included.

References

• Truth anchor: D5/S3/Factorization/PrimePowers/AffineGcdBehavior.affine_action_realization
• Truth anchor: D5/S3/Factorization/PrimePowers/AffineGcdBehavior.affine_word_translation
• Truth anchor: D5/S3/Factorization/PrimePowers/AffineGcdBehavior.local_encoding_complete
• Dependency: D5/S3/Arith/Congruence/PrimePowerAffineBehavior
• Dependency: D5/S3/Observer/Budget/PrimePowerNonadaptiveResolution
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality