Deletion Readout Inversion Constant

Abstract

Full-deletion readings determine every coordinate with an attained product constant.

Definition 1.1 (Deletion reading).

$$\begin{gathered} \forall r:\mathbb{N},m:(\mathrm{Fin}\left(r\right))\to \mathbb{N}, \\ T:\mathrm{Finset}\left(\mathrm{Fin}\left(r\right)\right),a:\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right),z:(\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right))\to \mathbb{R}, \\ R\left(T,a,z\right):=\sum _{c\in {\prod }_{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right)}z\left(c\right)\cdot \prod _{i\in T}{1}_{c_i\ne a_i}. \end{gathered}$$

Formalization. D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.R (✓ std3).

Source. Repository-derived.

Commentary.

For each selected coordinate, the factor vanishes exactly when the configuration takes the deleted value. Thus the sum retains precisely the configurations avoiding every prescribed value in T.

Definition 1.2 (Observation norm).

$$\begin{gathered} \forall r:\mathbb{N},m:(\mathrm{Fin}\left(r\right))\to \mathbb{N},\forall i\in \mathrm{Fin}\left(r\right),2\le m_i, \\ z:(\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right))\to \mathbb{R}, \\ \mathrm{obsNorm}\left(z\right):={\max }_{T\subseteq \mathrm{Fin}\left(r\right),a\in {\prod }_{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right)}|R\left(T,a,z\right)|. \end{gathered}$$

Formalization. D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.obsNorm (✓ std3).

Source. Repository-derived.

Commentary.

The maximum ranges over every coordinate subset and every dependent tuple of deleted values. The lower bound on each alphabet size makes this finite indexing family nonempty.

Definition 1.3 (Tensor inverse row sum).

$$\begin{gathered} \forall r:\mathbb{N},m:(\mathrm{Fin}\left(r\right))\to \mathbb{N}, \\ kappa(m):=\prod _{i\in \mathrm{Fin}\left(r\right)}(2-\frac{1}{m_i-1}). \end{gathered}$$

Formalization. D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.kappa (✓ std3).

Source. Repository-derived.

Commentary.

Each factor is the absolute row sum of J divided by m_i minus one, minus the identity. Their product is the tensor inverse row sum.

Theorem 1.4 (Sharp full-deletion inversion bound).

$$\begin{gathered} \forall r:\mathbb{N},m:(\mathrm{Fin}\left(r\right))\to \mathbb{N},\forall i\in \mathrm{Fin}\left(r\right),2\le m_i, \\ z:(\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right))\to \mathbb{R}, \\ (\forall c:\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right),|z\left(c\right)|\le \mathrm{kappa}\left(m\right)\cdot \mathrm{obsNorm}\left(z\right))\wedge \\ \forall c^{\ast }:\prod _{i\in \mathrm{Fin}\left(r\right)}\mathrm{Fin}\left(m_i\right), \\ \mathrm{let}w(c):=\prod _{i\in \mathrm{Fin}\left(r\right)}(\mathrm{if}{c}_i={c^{\ast }}_i\mathrm{then}2\cdot m_i-3\mathrm{else}-1), \\ \mathrm{obsNorm}\left(w\right)=\prod _{i\in \mathrm{Fin}\left(r\right)}(m_i-1)\wedge |w\left(c^{\ast }\right)|=\mathrm{kappa}\left(m\right)\cdot \mathrm{obsNorm}\left(w\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.deletion_readout_inversion_constant (✓ std3). ∎

Source. Repository-derived.

Commentary.

The coordinate matrix J minus I is inverted by J divided by m_i minus one, minus I. Tensoring these inverses reconstructs each coefficient from the full-deletion readings, and the absolute row sums factor.

For the displayed vector w, each coordinate sum is m_i minus two and each deleted coordinate sum has absolute value m_i minus one. Consequently every reading factors coordinatewise, the full deletion reading attains the observation norm, and the coefficient at the distinguished tuple attains the inversion bound.

References

• Truth anchor: D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.R
• Truth anchor: D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.deletion_readout_inversion_constant
• Truth anchor: D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.kappa
• Truth anchor: D5/S3/Arith/Congruence/DeletionReadoutInversionConstant.obsNorm