Affine modular stopping theorem 11.3

Abstract

The independent all-path affine modulus and exact named-edge stopping theorem.

Lemma 1.1 (Endpoint-preserving named-edge cycle erasure).

$$\forall \gamma \in \mathrm{Path}\left(v,w\right),\exists eta\in \mathrm{Path}\left(v,w\right):\mathrm{ActualSimple}\left(eta\right)\wedge \mathrm{Sublist}\left(\mathrm{edges}\left(eta\right),\mathrm{edges}\left(\gamma \right)\right)\wedge A\left(eta\right)\mid A\left(\gamma \right)\wedge \mathrm{length}\left(eta\right)\le |V|-1\wedge \forall p,\sum _{e\in eta}{\nu }_p(a_e)\le \sum _{e\in \gamma }{\nu }_p(a_e)$$

Proof. Machine-checked in Lean as D5/S3/Arith/AffineNetworks/AffineModularStopping.actual_cycle_erasure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every actual directed path has a simple actual path with the same endpoints. Its named-edge word is an occurrence sublist of the original word, its original multiplier product divides the original product, and its length is at most |V|−1. For every prime coordinate, erasure cannot increase the sum of edge losses, including the infinite loss of a zero multiplier.

The construction erases the prefix recursively. If the last edge ends at a vertex already in the erased prefix, it retains the actual prefix ending at that vertex. Otherwise it appends the same original named edge. Vertex-list uniqueness gives the cardinality bound; the surviving edge occurrences give product divisibility.

Theorem 1.2 (All-path prime-loss maximum and original gcd/lcm recurrence).

$$\forall v,0<D_v\wedge D_v\mid m;\forall v,p,\mathrm{Prime}\left(p\right)\wedge p\mid m⟹\forall w,\gamma \in \mathrm{Path}\left(v,w\right),{\nu }_p(\mathrm{quotient}\left(\gamma \right))=[{\nu }_p(d_w)-\sum _{e\in \gamma }{\nu }_p(a_e){]}_{+}\wedge {\nu }_p(D_v)=\underset{w\in V,\gamma \in \mathrm{Path}\left(v,w\right)}{\max }[{\nu }_p(d_w)-\sum _{e\in \gamma }{\nu }_p(a_e){]}_{+}=\underset{w\in V,\gamma \in \mathrm{Path}\left(v,w\right),\mathrm{ActualSimple}\left(\gamma \right),\mathrm{length}\left(\gamma \right)\le |V|-1}{\max }[{\nu }_p(d_w)-\sum _{e\in \gamma }{\nu }_p(a_e){]}_{+};\forall v,n,|V|-1\le n⟹\mathrm{iterate}\left(n,v\right)=D_v$$

Proof. Machine-checked in Lean as D5/S3/Arith/AffineNetworks/AffineModularStopping.theorem11_3 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let m be any positive integer, including 1. The nonempty finite vertex type and finite named-edge type retain loops and parallel edges. Each vertex source is the full ZMod m, with the reduction port modulo a positive divisor d_v of m. Every edge is legal on every phase and carries its original arbitrary natural multiplier a_e, including zero, and its affine offset c_e in ZMod m. A path transports the same phase through the original edge word; its multiplier A_γ is the product of those edge occurrences, with A_empty=1.

The modulus D_v is a positive divisor of m, independently defined as the lcm of d_w/gcd(d_w,A_γ) over all actual paths γ:v→w, with empty paths and prefixes retained. Its finite divisor image uses m.divisors and has no path-length truncation. For every prime p dividing m, ν_p(D_v) is the maximum of [ν_p(d_w)−Σ_e∈γ ν_p(a_e)]+ over all actual paths. The same maximum is attained on a simple actual path of length at most |V|−1. The loss convention is ν_p(0)=+∞ and [b−∞]+=0.

The recurrence is defined separately by D_v^(0)=d_v and D_v^(n+1) equal to the lcm of d_v and every D_w^(n)/gcd(D_w^(n),a_e) for the original outgoing named edges e:v→w. The proof characterizes its divisibility by the quotients of all paths of length at most n, using actual first-edge decomposition. Erasure then proves D_v^(n)=D_v for every n≥|V|−1. Empty outgoing-edge sets retain d_v.

The retained task records include all finite-path ports, prefixes and the empty path. Vertex and edge identities are public; control depends on obtained port records and internal state, and fixed fees are determined by the retained edge word. No phase guard, phase-dependent fee or extra reference is introduced. Erasure concerns the distinguishability kernel and may change offsets, outputs, visit counts and fees. Different primes can attain their maxima on different paths; the theorem does not assert one path attaining all prime optima.

References

• Truth anchor: D5/S3/Arith/AffineNetworks/AffineModularStopping.actual_cycle_erasure
• Truth anchor: D5/S3/Arith/AffineNetworks/AffineModularStopping.theorem11_3