Marked Charge Obstruction

Abstract

Marked Charge Obstruction

Theorem 1.1 (Marked Charge Obstruction).

$$\forall n\in \mathbb{N},\forall m\in \mathbb{N},\forall q\in \mathbb{N},\forall T\in \mathbb{Z},\left(\left(\left(\left(\mathrm{classS}\left(n\right)\wedge \mathrm{markedPrefix}\left(n,m,q,T\right)\right)\wedge \mathrm{mod}\left(n,2\right)=0\right)\wedge \mathrm{mod}\left(\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right),2\right)=0\right)\wedge \mathrm{PL}\left(\mathrm{ofFn}\left(\lambda i:\mathrm{Fin}\left(n\right)\mapsto \left(u_{\mathrm{pd}}\right)\left(\mathrm{val}\left(i\right)\right)\right)\right)=\mathrm{signedWeight}\left(\mathrm{cast}\left(\mathrm{div}\left(n+1,2\right),\mathbb{Z}\right)\right)\right)\Rightarrow 2\cdot \mathrm{sum}\left(\mathrm{range}\left(m\right),s:\mathbb{N}\mapsto 1+2\cdot \mathrm{cast}\left(\mathrm{mod}\left(q+3\cdot s,2\right),\mathbb{Z}\right)\right)\le \mathrm{cast}\left(\mathrm{signedDigitCharge}\left(n\right),\mathbb{Z}\right)+2\cdot \mathrm{cast}\left(\mathrm{mod}\left(q,2\right),\mathbb{Z}\right)\cdot \mathrm{ite}\left(2\cdot T-\mathrm{cast}\left(\mathrm{mod}\left(n,2\right),\mathbb{Z}\right)<0,1,0\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/MarkedPathObstruction.marked_charge_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

A class-S endpoint of even parity and even signed weight can attain its signed-weight lower bound only if twice its marked-prefix weight fits inside the signed-digit charge plus the lower-tail phase correction. The proof follows an optimal tight path and accounts for each removed marked digit. div and mod denote natural integer quotient and remainder; cast explicitly denotes the displayed coercions.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPathObstruction.marked_charge_obstruction
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/EvenTightPaths
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/MarkedPrefixRigidity
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/TightFactorization