OP5 Pareto Stop Equivalences Are Refuted

Abstract

A complete sourced two-action model refutes both OP5 Pareto linear-extension stop equivalences.

Theorem 1.1 (Dominance direction reverses the proposed stop characterizations).

$$\left(\mathrm{Nonempty}\left(\mathrm{feasible}\left(\right)\right)\wedge \left(\mathrm{feasible}\left(\mathrm{decision}\left(\mathrm{commitment}\left(\right)\right)\right)=\mathrm{feasible}\left(\right)\wedge \left(\mathrm{current}\left(\mathrm{decision}\left(\mathrm{commitment}\left(\right)\right)\right)=\mathrm{some}\left(true\right)\wedge \left(\left(\forall action\in \mathrm{Bool}\left(\right),action\in \mathrm{feasible}\left(\right)\Rightarrow \left(action\in \mathrm{admissibleTarget}\left(\mathrm{goal}\left(\mathrm{paretoOrientation}\left(\right)\right)\right)\wedge \mathrm{inScope}\left(\mathrm{scope}\left(\mathrm{paretoOrientation}\left(\right)\right),action\right)\right)\right)\wedge \left(\mathrm{ParetoMaximalIn}\left(\mathrm{value}\left(\right),\mathrm{feasible}\left(\right),true\right)\wedge \left(\mathrm{ParetoGreatestIn}\left(\mathrm{value}\left(\right),\mathrm{feasible}\left(\right),true\right)\wedge \mathrm{Nonempty}\left(\mathrm{LinearExtension}\left(\right)\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\neg \left(\mathrm{ParetoMaximalIn}\left(\mathrm{value}\left(\right),\mathrm{feasible}\left(\right),true\right)\iff \left(\exists L\in \mathrm{LinearExtension}\left(\right),\mathrm{OrientedStop}\left(\mathrm{admissibleTarget}\left(\right),\mathrm{InFiniteNarrowedScope}\left(\mathrm{inScope}\left(\right)\right),\mathrm{orientation}\left(L\right),\mathrm{commitment}\left(\right)\right)\right)\right)\right)\wedge \left(\neg \left(\left(\forall L\in \mathrm{LinearExtension}\left(\right),\mathrm{OrientedStop}\left(\mathrm{admissibleTarget}\left(\right),\mathrm{InFiniteNarrowedScope}\left(\mathrm{inScope}\left(\right)\right),\mathrm{orientation}\left(L\right),\mathrm{commitment}\left(\right)\right)\right)\iff \mathrm{ParetoGreatestIn}\left(\mathrm{value}\left(\right),\mathrm{feasible}\left(\right),true\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoLinearExtensionStopRefutation.op5_pareto_stop_linear_extension_equivalences_refuted (✓ std3). ∎

Source. Repository-derived.

Commentary.

The feasible carrier is Bool and the current action is true. True has strictly better values in all three benefit coordinates and strictly lower values in both cost coordinates, so it is both Pareto-maximal and Pareto-greatest under the frozen dominance convention.

Each LinearExtension value contains a complete linear order on the explicit finite Pareto quotient, a proof that it extends QuotientParetoWeak, and a full OrientationSpec. The latter preserves goal, source, and version and records the narrowed scope as the original scope paired with the feasible Finset.

A Szpilrajn extension witnesses that the extension family is nonempty. Every member places the dominating true class before the false class. OrientedStop rejects strict successors of current, hence no member stops at true and both displayed equivalences fail.

The displayed certificate includes every OP5 side condition: nonempty feasibility, the sealed feasible/current fields, admissibility and original-scope membership, maximality, greatestness, and extension nonemptiness. Repository, pinned-Mathlib, and third-party searches found no existing theorem with this sourced-stop statement.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/ParetoLinearExtensionStopRefutation.op5_pareto_stop_linear_extension_equivalences_refuted
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/AdjudicationStopTargetCorrectness
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeAdjudication/QuotientParetoWeakOrder