Actual Anchored Recursive Supply

Abstract

A full literal label tuple supplies actual recursive boundary ports, their native c edges, and their distinctness.

Definition 1.1 (Independent Full Label Frames).

$$\mathrm{SupplyFrame}\left(m,k\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.SupplyFrame (✓ std3).

Source. Repository-derived.

Commentary.

SupplyFrame(m,k) contains selected and base lists and a terminal label. The selected list has length k; selected followed by base has length m. The full tuple selected, base, terminal is nodup and contains every label in Fin(m+1). The frame does not contain a path, coverage premise, or recursive construction certificate.

Definition 1.2 (The Actual Literal Anchor).

$$\mathrm{Tuple}\left(\mathrm{anchor}\left(F\right)\right)=\mathrm{Append}\left(\mathrm{Append}\left(\mathrm{Selected}\left(F\right),\mathrm{Base}\left(F\right)\right),\mathrm{Singleton}\left(\mathrm{Terminal}\left(F\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.anchor (✓ std3).

Source. Repository-derived.

Commentary.

The nodup complete tuple determines an actual permutation of Fin(m+1), with precisely selected followed by base followed by the terminal as its literal list.

Definition 1.3 (Actual Right Supply Ports).

$$\mathrm{rightPort}\left(F,i\right)=\mathrm{Multiply}\left(\mathrm{anchor}\left(F\right),\mathrm{Power}\left(\mathrm{Multiply}\left(\mathrm{b}\left(m\right),\mathrm{c}\left(m\right)\right),i\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.rightPort (✓ std3).

Source. Repository-derived.

Commentary.

R_i is anchor(F) multiplied on the right by (b_m c_m)^i. Its prefix rotates forward by i and its terminal label stays fixed.

Definition 1.4 (Actual Left Supply Ports).

$$\mathrm{leftPort}\left(F,i\right)=\mathrm{Multiply}\left(\mathrm{rightPort}\left(F,i\right),\mathrm{b}\left(m\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.leftPort (✓ std3).

Source. Repository-derived.

Commentary.

L_i is R_i b_m. It reverses the entire prefix and keeps the terminal; the base is not independently reversed in the frame.

Definition 1.5 (The Distinguished k Plus One Port Pairs).

$$\mathrm{specialPort}\left(F,p\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.specialPort (✓ std3).

Source. Repository-derived.

Commentary.

For p in Fin(k+1) times Fin(2), side zero selects R at p’s first coordinate and side one selects L at that same coordinate.

Theorem 1.6 (Every Supply Coordinate and Closing Seam Is Actual).

$$\forall m\in \mathrm{Nat},3\le m\Rightarrow \left(\forall k\in \mathrm{Nat},\forall F\in \mathrm{SupplyFrame}\left(m,k\right),\left(\forall i\in \mathrm{Nat},\mathrm{Tuple}\left(\mathrm{rightPort}\left(F,i\right)\right)=\mathrm{Append}\left(\mathrm{Rotate}\left(\mathrm{Append}\left(\mathrm{Selected}\left(F\right),\mathrm{Base}\left(F\right)\right),i\right),\mathrm{Singleton}\left(\mathrm{Terminal}\left(F\right)\right)\right)\wedge \left(\mathrm{Tuple}\left(\mathrm{leftPort}\left(F,i\right)\right)=\mathrm{Append}\left(\mathrm{Reverse}\left(\mathrm{Rotate}\left(\mathrm{Append}\left(\mathrm{Selected}\left(F\right),\mathrm{Base}\left(F\right)\right),i\right)\right),\mathrm{Singleton}\left(\mathrm{Terminal}\left(F\right)\right)\right)\wedge \left(\mathrm{Multiply}\left(\mathrm{leftPort}\left(F,i\right),\mathrm{c}\left(m\right)\right)=\mathrm{rightPort}\left(F,\mathrm{Add}\left(i,1\right)\right)\wedge \mathrm{Adj}\left(\mathrm{NativeCayleyGraph}\left(m\right),\mathrm{leftPort}\left(F,i\right),\mathrm{rightPort}\left(F,\mathrm{Add}\left(i,1\right)\right)\right)\right)\right)\right)\wedge \left(\mathrm{Multiply}\left(\mathrm{leftPort}\left(F,\mathrm{Subtract}\left(m,1\right)\right),\mathrm{c}\left(m\right)\right)=\mathrm{rightPort}\left(F,0\right)\wedge \mathrm{Adj}\left(\mathrm{NativeCayleyGraph}\left(m\right),\mathrm{leftPort}\left(F,\mathrm{Subtract}\left(m,1\right)\right),\mathrm{rightPort}\left(F,0\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.native_anchored_supply_coordinates (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every m at least three, every k, every full SupplyFrame(m,k), and every natural supply position i, the right tuple is rotate(selected ++ base,i) followed by terminal. The left tuple is the reverse of that same prefix followed by terminal. Multiplication by the actual c generator takes L_i to R_(i+1), and these configurations are adjacent in the actual Cayley graph generated by a, b and c. The final full-supply seam takes L_(m-1) to R_0 and is also a native edge.

The tuple and generator formulas are proved from the actual permutation coordinates. Full supplier closure uses the earned order-m prefix rotation. The c generator is nonidentity when m is at least three. No abstract boundary graph is supplied as a premise. This theorem does not assert a Hamilton cycle, a prior-cycle edge inventory, or the recursive all-size closure.

Theorem 1.7 (Every Distinguished Actual Port Is Distinct When k Is Below m).

$$\forall m\in \mathrm{Nat},3\le m\Rightarrow \left(\forall k\in \mathrm{Nat},\forall F\in \mathrm{SupplyFrame}\left(m,k\right),k<m\Rightarrow \mathrm{Injective}\left(\mathrm{specialPort}\left(F\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.native_special_port_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

For m at least three and k strictly below m, the actual specialPort map on Fin(k+1) times Fin(2) is injective. The proof embeds these ports into the existing native supplier coordinate equivalence, so distinctness concerns actual configurations. The strict k < m condition is necessary: the full supplier returns to R_0 at index m.

References

• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.SupplyFrame
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.anchor
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.leftPort
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.native_anchored_supply_coordinates
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.native_special_port_injective
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.rightPort
• Truth anchor: D5/S3/Combinatorics/Graph/PrefixReversal/NativeRecursiveSupply.specialPort
• Dependency: D5/S3/Combinatorics/Graph/PrefixReversal/NativeCircleOwnership
• Dependency: D5/S3/Combinatorics/Graph/PrefixReversal/NativeSwitches