Exact Native Unary Block Exchanges

Abstract

Every minimum unary-source mask has exact descent under every admissible exchange.

The first source is inserted and the second source is the base. Both are nonempty. A native admissible cut exchanges two whole adjacent maximal runs with the required exterior U-run. Either source may be unary; the two orientations are proved with their distinct degree formulas.

Theorem 1.1 (Lower bound for every exchange).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall u\in \mathrm{List}\left(alpha\right),\forall v\in \mathrm{List}\left(alpha\right),\forall E\in \mathrm{BlockCut}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\forall a\in alpha,\forall n\in \mathrm{Nat}\left(\right),\left(u\ne nil\wedge \left(\mathrm{ValidMask}\left(u,v,\mathrm{original}\left(E\right),M\right)\wedge \left(\mathrm{Admissible}\left(E,M\right)\wedge \left(u=\mathrm{replicate}\left(n,a\right)\vee v=\mathrm{replicate}\left(n,a\right)\right)\right)\right)\right)\Rightarrow \left(\exists s\in \mathrm{Nat}\left(\right),\exists t\in \mathrm{Nat}\left(\right),\mathrm{degree}\left(u,v,\mathrm{original}\left(E\right)\right)=s\wedge \left(\mathrm{degree}\left(u,v,\mathrm{successor}\left(E\right)\right)=t\wedge s\le t+1\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryExchange.exchange_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

Delete the actual block whose label belongs to the unary source. Its letters are all a, and the deleted word has both reduced ordered source projections. The old and exchanged words reinsert the same mass at two actual cuts. The indexed gap transport identifies the changed gap at each cut, including cuts separated by any number of zero-mass gaps. Adding mass increases the occupied-gap count by at most one; in the reverse orientation only internal gaps contribute. This gives the lower bound without assuming commutation of the non-unary projection.

Theorem 1.2 (Every minimum mask and every exchange).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall u\in \mathrm{List}\left(alpha\right),\forall v\in \mathrm{List}\left(alpha\right),\forall E\in \mathrm{BlockCut}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\forall r\in \mathrm{Nat}\left(\right),\left(u\ne nil\wedge \left(v\ne nil\wedge \left(\mathrm{IsMinimumMask}\left(u,v,\mathrm{original}\left(E\right),M,r\right)\wedge \left(2\le r\wedge \left(\mathrm{Admissible}\left(E,M\right)\wedge \left(\left(\exists a\in alpha,\exists m\in \mathrm{Nat}\left(\right),1\le m\wedge u=\mathrm{replicate}\left(m,a\right)\right)\vee \left(\exists a\in alpha,\exists n\in \mathrm{Nat}\left(\right),1\le n\wedge v=\mathrm{replicate}\left(n,a\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{degree}\left(u,v,\mathrm{successor}\left(E\right)\right)=\mathrm{NatSub}\left(r,1\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/HughesUnaryExchange.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every r>1, every minimum mask M and every admissible cut E, the successor degree is exactly r-1. The common-deletion lower bound gives at least r-1. The original native intended-successor theorem gives a valid successor mask with exactly r-1 U-runs and hence the matching upper bound. Both exchange directions are included. No choice of a preferred minimum mask is made, and no statement about an empty inserted source is inferred.

References

• Truth anchor: D5/S1/Words/HughesUnaryExchange.exchange_lower
• Truth anchor: D5/S1/Words/HughesUnaryExchange.result
• Dependency: D5/S1/Words/HughesUnaryInsertion