Correctness and Path Legitimacy

Abstract

Equal correct results cannot determine opposite path legitimacy.

Theorem 1.1 (A correct result does not determine path legitimacy).

$\forall G amma, R, r : G amma \to R, C, L : G amma \to P ro p, g amm a_{a}, g amm a_{u} \in G amma, r (g amm a_{a}) = r (g amm a_{u}) \land C (g amm a_{a}) \land C (g amm a_{u}) \land L (g amm a_{a}) \land \neg L (g amm a_{u}) \Rightarrow \neg\exists D : R \to P ro p, \forall g amma \in G amma, C (g amma) \Rightarrow (D (r (g amma)) ⟺ L (g amma)) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Audits/CorrectnessLegitimacySeparation.correct_result_does_not_determine_legitimacy (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take two paths that reach the same result and satisfy the same correctness predicate. The first path is legitimate and the second is not.

Any proposed predicate of results must assign the same proposition to both paths because their results are equal. Agreement with legitimacy on all correct paths would therefore both accept and reject that common result, which is impossible.

The path predicates and result map are independent inputs, so legitimacy is not defined from the desired non-determination conclusion. The proof directly applies equality transport from the pinned library.

Repository and pinned-library searches found no exact theorem combining equal correct results, opposite path legitimacy, and result-only decision failure.

References

Truth anchor: D5/S3/ConceptDynamics/Audits/CorrectnessLegitimacySeparation.correct_result_does_not_determine_legitimacy
Dependency: D5/S3/ConceptDynamics/LegitimacyCorrectness

Keyboard shortcuts

trureturing Blueprint

Correctness and Path Legitimacy

Abstract

References