Canonical Verdict Reduction

Abstract

Verdict tables descend canonically, reduce by column representatives, and remain relative to the implementation population.

Theorem 1.1 (The true verdict source is its population-relative double quotient).

$\forall I m pl e m e n t a t i o n, T es t : Type, r : I m pl e m e n t a t i o n \to (T es t \to Bool), let im pl e m e n t a t i o n Ker n e l := ker (λi : I m pl e m e n t a t i o n, λ t : T es t, r (i, t)), t es t Ker n e l := ker (λ t : T es t, λi : I m pl e m e n t a t i o n, r (i, t)), c an o ni c a l V er d i c t : Quotient (im pl e m e n t a t i o n Ker n e l) \to (Quotient (t es t Ker n e l) \to Bool) := QuotientLift2 (r, im pl e m e n t a t i o n Ker n e l, t es t Ker n e l) in (\forall i : I m pl e m e n t a t i o n, j : I m pl e m e n t a t i o n, t : T es t, u : T es t, im pl e m e n t a t i o n Ker n e l (i, j) \land t es t Ker n e l (t, u) \Rightarrow r (i, t) = r (j, u)) \land (\forall i : I m pl e m e n t a t i o n, t : T es t, c an o ni c a l V er d i c t (class (i), class (t)) = r (i, t)) \land (\forall f : Quotient (im pl e m e n t a t i o n Ker n e l) \to (Quotient (t es t Ker n e l) \to Bool), (\forall i : I m pl e m e n t a t i o n, t : T es t, f (class (i), class (t)) = r (i, t)) \Rightarrow f = c an o ni c a l V er d i c t) \land (\forall k e pt : Set (T es t), ((\forall t : T es t, \exists q, q \in k e pt \land t es t Ker n e l (q, t)) \land (\forall c an d i d a t e : Set (T es t), c an d i d a t e \subseteq k e pt \land (\forall t : T es t, \exists q, q \in c an d i d a t e \land t es t Ker n e l (q, t)) \Rightarrow k e pt \subseteq c an d i d a t e)) ⟺ (\forall t : T es t, \exists! q, q \in k e pt \land t es t Ker n e l (q, t))) \land (\forall t : T es t, u : T es t, t \neq = u \land t es t Ker n e l (t, u) \Rightarrow \exists r P r im e : Option (I m pl e m e n t a t i o n) \to (T es t \to Bool), (\forall i : I m pl e m e n t a t i o n, r P r im e (some (i)) = r (i)) \land r P r im e (n o n e, t) \neq = r P r im e (n o n e, u)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/VisibleDescent/CanonicalVerdictReduction.canonical_verdict_reduction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The implementation kernel is equality of complete verdict rows, and the test kernel is equality of complete verdict columns. Mathlib’s two-quotient lift gives the displayed canonical verdict map; its representative computation rule determines that map uniquely.

A retained test subset is lossless when every original test has a retained test with the same column. Such a subset is inclusion-minimal among lossless subsets exactly when it contains one representative of every column class.

Two distinct tests can agree on every current implementation and cease to agree after one implementation is adjoined. Redundancy is therefore indexed by the chosen implementation population.

The canonical descent and extension witness are imported from their frozen D5 owners. Repository and pinned-Mathlib searches found no existing minimal-lossless-subset characterization with this verdict-column shape.

References

Truth anchor: D5/S3/Observer/VisibleDescent/CanonicalVerdictReduction.canonical_verdict_reduction
Dependency: D5/S0/Naming/VerdictColumnSeparation
Dependency: D5/S3/Observer/Refinement/DoubleExtensionalEvaluationDescent

Keyboard shortcuts

trureturing Blueprint

Canonical Verdict Reduction

Abstract

References