Closure, Method Stop, and Three-Parameter Completion/Reopening

Abstract

Exact and approximate closure support method stopping and three-parameter completion/reopening.

Theorem 1.1 (Closure, method stop, and three-parameter completion/reopening).

$$\left(\mathrm{Closed}\left(q,T\right)\iff \mathrm{defectRelation}\left(q,T\right)=\varnothing \right)\wedge \left(\left([\mathrm{MetricSpace}(T)]\Rightarrow \left(\mathrm{ApproximatelyClosed}\left(q,T,(\epsilon :\mathrm{NNReal})\right)\iff \mathrm{worstFiberDefect}\left(q,T\right)\le \mathrm{coeENNReal}\left((\epsilon :\mathrm{NNReal})\right)\right)\right)\wedge \left(\left(\mathrm{MethodStopped}\left(M,S,E,NoProposal\right)\iff M\left(S,E\right)=NoProposal\right)\wedge \left(\left([\mathrm{MetricSpace}(T)]\Rightarrow \left(\mathrm{ThreeParameterLocallyComplete}\left(P,q\right)\iff \mathrm{ApproximatelyClosed}\left(\mathrm{restrict}\left(q,\mathrm{objectDomain}\left(P\right)\right),\mathrm{restrict}\left(\mathrm{target}\left(P\right),\mathrm{objectDomain}\left(P\right)\right),\mathrm{precision}\left(P\right)\right)\right)\right)\wedge \left([\mathrm{MetricSpace}(T)]\Rightarrow \left(\mathrm{ThreeParameterReopens}\left(P0,P1,q\right)\iff \left(\left(\mathrm{objectDomain}\left(P0\right)\ne \mathrm{objectDomain}\left(P1\right)\vee \left(\mathrm{target}\left(P0\right)\ne \mathrm{target}\left(P1\right)\vee \mathrm{precision}\left(P0\right)\ne \mathrm{precision}\left(P1\right)\right)\right)\wedge \mathrm{Nonempty}\left((\mathrm{inter}\left(\mathrm{inter}\left(\mathrm{defectRelation}\left(q,\mathrm{target}\left(P1\right)\right),\mathrm{distanceAbove}\left(\mathrm{target}\left(P1\right),\mathrm{precision}\left(P1\right)\right)\right),\mathrm{square}\left(\mathrm{objectDomain}\left(P1\right)\right)\right))\setminus (\mathrm{inter}\left(\mathrm{inter}\left(\mathrm{defectRelation}\left(q,\mathrm{target}\left(P0\right)\right),\mathrm{distanceAbove}\left(\mathrm{target}\left(P0\right),\mathrm{precision}\left(P0\right)\right)\right),\mathrm{square}\left(\mathrm{objectDomain}\left(P0\right)\right)\right))\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Termination/ClosureMethodStopThreeParameterCompletionReopening.closure_method_stop_three_parameter_completion_reopening (✓ std3). ∎

Source. Repository-derived.

Commentary.

The package records five formalized assertions. Target closure uses the canonical defectRelation; approximate closure uses the supremum of metric target diameters over readout fibers against a finite nonnegative tolerance chosen by this formalization. Empty fibers contribute zero and unbounded diameters contribute top. Method stopping is the literal distinguished-value equation.

Three-parameter local completion checks the supplied domain, target, and finite precision. A three-parameter reopening requires one of those parameters to change and a canonical defect pair above the next precision that was absent above the current precision.

Unresolved source gaps: section 5 defines a language-blind residual and section 44 defines operation-induced observational equivalence, but section 43 does not identify either construction with its stage readout or residual, nor give a transition map to a new stage residual. This formalization covers only the object-domain, target, and precision triggers.

Section 9.1 assumes a metric and explicitly uses tolerance zero, but it does not type the tolerance or decide whether negative tolerances are allowed. Lean conventionally uses NNReal; this is not presented as an exact source-domain match and must be reopened if the source later admits negative tolerance.

No finiteness, decidable equality, measurability, nonempty-domain premise, monotonicity, or extra order law is added. The target metric is exactly the structure requested by approximate closure.

References

• Truth anchor: D5/S3/ConceptDynamics/Termination/ClosureMethodStopThreeParameterCompletionReopening.closure_method_stop_three_parameter_completion_reopening
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff