Executable Refinement Matrix

Abstract

An ordered state enumeration makes every false refinement cell executable, deterministic, and proof-backed.

Definition 1.1 (Kernel comparison cases).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.KernelComparison

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.KernelComparison (✓ std3).

Source. Repository-derived.

Commentary.

The four cases distinguish equality, either strict direction, and incomparability.

Definition 1.2 (Classified kernel comparison).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.kernelComparison

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.kernelComparison (✓ std3).

Source. Repository-derived.

Commentary.

The two decidable inclusion cells determine the four-way classification.

Definition 1.3 (Executable refinement witness).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness (✓ std3).

Source. Repository-derived.

Commentary.

Spec spelling refinementWitness?. The search uses states.product states, visiting the outer-left state first and the inner-right state second.

Theorem 1.4 (The selector uses the documented pair order).

$$\mathrm{refinementWitness}(C,E,i,j)=\mathrm{find}(\mathrm{product}(\mathrm{states}(E),\mathrm{states}(E)),\mathrm{separatesRefinement}(C,i,j)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_order (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from executable ordered search and Boolean agreement reflection.

Theorem 1.5 (No witness exactly means refinement).

$$\mathrm{refinementWitness}(C,E,i,j)=\mathrm{none}()\iff \mathrm{KernelRefines}(C,i,j).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_eq_none_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from executable ordered search and Boolean agreement reflection.

Theorem 1.6 (A returned refinement witness is sound).

$$\mathrm{refinementWitness}(C,E,i,j)=\mathrm{some}(p)\Rightarrow \left(\mathrm{agrees}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),\mathrm{fst}(p),\mathrm{snd}(p))\wedge \neg \mathrm{agrees}(\mathrm{primitives}(\mathrm{theoremAt}(C,j)),\mathrm{fst}(p),\mathrm{snd}(p))\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_eq_some_implies (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from executable ordered search and Boolean agreement reflection.

Theorem 1.7 (A false cell has a deterministic witness).

$$(\exists p,\mathrm{refinementWitness}(C,E,i,j)=\mathrm{some}(p))\iff \neg \mathrm{KernelRefines}(C,i,j).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_exists_iff_not_kernelRefines (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from executable ordered search and Boolean agreement reflection.

Theorem 1.8 (Kernel comparison carries all inclusion and witness payloads).

$$(\mathrm{kernelComparison}(C,i,j)=equal\iff \mathrm{KernelRefines}(C,i,j)\wedge \mathrm{KernelRefines}(C,j,i))\wedge \left((\mathrm{kernelComparison}(C,i,j)=strictlyFiner\iff \mathrm{KernelRefines}(C,i,j)\wedge (\exists p,\mathrm{refinementWitness}(C,E,j,i)=\mathrm{some}(p)))\wedge \left((\mathrm{kernelComparison}(C,i,j)=strictlyCoarser\iff (\exists p,\mathrm{refinementWitness}(C,E,i,j)=\mathrm{some}(p))\wedge \mathrm{KernelRefines}(C,j,i))\wedge (\mathrm{kernelComparison}(C,i,j)=incomparable\iff (\exists p,\mathrm{refinementWitness}(C,E,i,j)=\mathrm{some}(p))\wedge (\exists p,\mathrm{refinementWitness}(C,E,j,i)=\mathrm{some}(p)))\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.kernelComparison_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from executable ordered search and Boolean agreement reflection.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.KernelComparison
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.kernelComparison
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.kernelComparison_spec
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_eq_none_iff
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_eq_some_implies
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_exists_iff_not_kernelRefines
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/RefinementMatrix.refinementWitness_order
• Dependency: D5/S3/ConceptDynamics/InformationEscapeCounting/Fused
• Dependency: D5/S3/ConceptDynamics/InformationEscapeHierarchy/AnalysisLaws