Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Successor-chain stopping sharpness

Abstract

An actual named successor chain attains the original modular stopping depth.

Theorem 1.1 (Original recurrence and complete actual-source transcripts).

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

Source. Repository-derived.

Commentary.

For every natural N≥2 and m≥2, the theorem constructs one actual Network C. Its vertex and named-edge types are equivalent to Fin N and Fin (N−1). Edge j has source rank j and destination rank j+1, multiplier 1 and offset 0. The root has rank 0, the last vertex rank N−1, the ambient modulus is m, and exactly the last vertex has port m; every other port is 1.

Notation in the authored formula follows the original Lean objects: Nat is ℕ, Equiv(A,B) is A≃B, Type(u) uses the theorem’s arbitrary universe u, and a binder displayed with ∈ is a typed binder. Network, NPath, networkQuiver, iterate, pathRun and portRead are the original AffineModularStopping declarations. Dotted names and numeric projections are the original record fields and tuple projections; in particular val(iv(v)) is a rank, while v itself lies in C.V. List, Sum, Option and Prod are the corresponding Lean types. Σ v:T,U is the dependent pair type Sigma, angle brackets construct such pairs, parentheses construct ordinary pairs, brackets construct lists, and ++ is List.append. A colon is a type ascription; if(b,x,y) means if b then x else y. Path.nil, path.cons, path.comp, Sum.inl, Sum.inr, none, some and HEq are the original constructors, path operations and heterogeneous equality. The typed let and match bind state and next locally, with their usual Lean stop/append branches. The trace endpoint arguments are implicit in Lean; their dependent function domain is displayed explicitly here.

The independently defined original gcd/lcm iterate is evaluated for every depth n and every vertex of rank i. It equals 1 when i+n<N−1 and m otherwise. The proof computes the actual outgoing named-edge subtype: empty at the last vertex and a singleton elsewhere. Depth induction propagates the terminal port; no replacement recurrence or assumed path characterization is used.

Every actual path from v to w satisfies rank(w)=rank(v)+length(path), and its original phase run preserves every t in the full source ZMod m. An actual root-to-last named-edge path is constructed with length N−1. Its terminal port returns the original canonical phase residue and separates the same sources 0 and 1 used in every shorter experiment.

For every shorter root path, every factorization into a prefix and a suffix has prefix port 1 and equal actual reads for 0 and 1. The empty prefix gives the initial root read; the empty suffix gives the final read of that path. The chronological trace has typed vertex-port events and named-edge events. It starts with the actual root read and appends each actual edge followed by the read of the same continuously transported phase at its destination. The displayed trace equations use the same C and trace bound in the statement.

For every internal-control type K and every deterministic choice function of public vertex, current control and obtained chronological trace, an actual executor is constructed. Choices are either stop or an original legal outgoing arrow with its next control state. The returned state retains the actual path and control. At zero it is the root empty path and the supplied common control; each next step either stays stopped or appends the chosen named arrow. The executed path length is at most the step count. At every count below N−1, both sources produce equal paths, controls, complete chronological traces and next choices. This is proved by induction from actual prefix reads, rather than assuming transcript equality. A common external random seed may be included in K; the theorem states deterministic equality for each fixed seed.

At every shorter depth , the same original root iterate is 1, while its value at N−1 is m≠1. The explicit delayed distinguishing experiment therefore prevents any smaller uniform stopping depth. This statement concerns the prescribed finite full-phase network and history-based legal control. It adds no hidden phase guards, costs or reference channels, and makes no claim about the cost of obtaining a complete behavior boundary.

References