Arbitrary Coordinate Erasure Criterion

Abstract

Worst-case residue erasure capacity is the product of the smallest survivors.

Theorem 1.1 (Every coordinate erasure pattern is faithful at prefix capacity).

$$\begin{array}{c}\forall m:\mathbb{N}\to \mathbb{N},n,K:\mathbb{N},\\ s:\mathrm{Fin}(n+1),\\ \forall i<n,2\le m(i)\wedge \\ \forall i,j<n,i<j\Rightarrow m(i)<m(j)\wedge \\ \forall i,j<n,i\ne j\Rightarrow \mathrm{Coprime}(m(i),m(j))\Rightarrow \\ \forall R:\mathrm{Finset}(\mathrm{Fin}(n)),\mathrm{card}(R)=n-s\Rightarrow \mathrm{Injective}(\mathrm{jointReadout}(\Lambda i:R,\Lambda x:\mathrm{Fin}(K),\mathrm{castZMod}(\mathrm{val}(x),m(\mathrm{val}(i)))))⟺K\le \prod _{i:\mathrm{Fin}(n-s)}m(i)\wedge \\ \forall R:\mathrm{Finset}(\mathrm{Fin}(n)),\mathrm{card}(R)=n-s\Rightarrow \prod _{i:\mathrm{Fin}(n-s)}m(i)\le \prod _{i\in R}m(\mathrm{val}(i)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ResidueCoding/ArbitraryCoordinateErasureCriterion.arbitrary_coordinate_erasure_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The readout on each retained coordinate set is the canonical joint readout of the corresponding residue channels.

The retained-set recovery criterion reduces injectivity to product capacity. Sortedness then proves that the first surviving prefix has no larger product than any equally sized set.

References

• Truth anchor: D5/S3/ConceptDynamics/ResidueCoding/ArbitraryCoordinateErasureCriterion.arbitrary_coordinate_erasure_criterion
• Dependency: D5/S3/Arith/Coding/ResidueCodeDynamicRange
• Dependency: D5/S3/ConceptDynamics/ResidueCoding/RetainedResidueRecoveryCriterion