Retained Residue Recovery Criterion

Abstract

Retained coprime residue coordinates recover a bounded state exactly when their product has sufficient capacity.

Theorem 1.1 (Retained residues are injective exactly at product capacity).

$$\begin{array}{c}\forall R,m,K,\\ \mathrm{Finite}(R)\wedge (\forall i\in R,0<m_i)\wedge \mathrm{PairwiseCoprime}(m)\Rightarrow \\ \mathrm{Injective}(\mathrm{jointReadout}(i\mapsto x\mapsto x\mathrm{mod}{m}_i):X_K\to \prod _{i\in R}\mathrm{ZMod}(m_i))⟺K\le \prod _{i\in R}{m}_i.\end{array}$$

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

Source. Repository-derived.

Commentary.

Let R be the finite family of retained coordinates. Each retained modulus is positive, and distinct retained moduli are coprime.

The observation is the canonical dependent joint readout whose ith coordinate reduces a bounded natural state modulo the ith modulus.

Injectivity forces the state-space cardinality not to exceed the product of the output cardinalities. Conversely, the finite-family Chinese remainder equivalence identifies equal residue words modulo the product, and the capacity bound makes the representatives equal.

References

• Truth anchor: D5/S3/ConceptDynamics/ResidueCoding/RetainedResidueRecoveryCriterion.retained_residue_recovery_iff_product_capacity
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion