Oracle Intervention-Law Error Detection

Abstract

Exact intervention-law codewords decode uniquely below half their minimum coordinate distance.

Theorem 1.1 (Oracle intervention-law errors have a unique decoding).

$$\begin{array}{r}\forall Model,Law:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(Law\right)],\\ n,e\in \mathbb{N},\\ law:\mathrm{Fin}\left(n\right)\to \left(Model\to Law\right),\\ M:Model,r:\mathrm{Fin}\left(n\right)\to Law,\\ \mathrm{hammingDist}\left(r,\mathrm{jointReadout}\left(law,M\right)\right)\le e\wedge 2\times e<\mathrm{interventionMinimumDistance}\left(law\right)\Rightarrow \\ \exists !c:\mathrm{Fin}\left(n\right)\to Law,\\ c\in \mathrm{range}\left(\mathrm{jointReadout}\left(law\right)\right)\wedge \mathrm{hammingDist}\left(r,c\right)\le e.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionLaws/OracleLawErrorDetection.oracle_intervention_law_error_detection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite law suite sends each model to its canonical jointReadout codeword. Its minimum distance is constructed as the least Hamming distance between codewords arising from distinct models.

If the received law word differs from the true model codeword in at most e coordinates, any competing codeword in the same radius lies within 2e coordinates of it. The strict minimum-distance condition forces the competing codeword to equal the true one.

References

• Truth anchor: D5/S3/ConceptDynamics/InterventionLaws/OracleLawErrorDetection.oracle_intervention_law_error_detection
• Dependency: D5/S3/Arith/Coding/UniqueDecodingRadius
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion