Semantic Target-Laundering Decision

Abstract

Decidable protected coordinates and report conditions yield an exact laundering decision.

Theorem 1.1 (The laundering predicate has a certified Boolean decision).

$$\begin{array}{c}\forall Commitment,Evidence,Verdict,Time,TargetChain,Domain,Epsilon,Condition,Comparator,Baseline,WeightSpec,Report:\mathrm{Type},\\ [\mathrm{LT}\left(Time\right)],\\ [\mathrm{DecidableEq}\left(Commitment\right)],[\mathrm{DecidableEq}\left(Evidence\right)],\\ [\mathrm{DecidableEq}\left(TargetChain\right)],[\mathrm{DecidableEq}\left(Domain\right)],[\mathrm{DecidableEq}\left(Epsilon\right)],\\ [\mathrm{DecidableEq}\left(Condition\right)],[\mathrm{DecidableEq}\left(Comparator\right)],[\mathrm{DecidableEq}\left(Baseline\right)],[\mathrm{DecidableEq}\left(WeightSpec\right)],\\ [\mathrm{DecidableRel}\left((\cdot <\cdot ):Time\to Time\to Prop\right)],\\ S:\mathrm{RegradeSemantics}\left(Commitment,Evidence,Verdict,Time,\mathrm{ProtectedCoordinates}\left(TargetChain,Domain,Epsilon,Condition,Comparator,Baseline,WeightSpec\right),Report\right),\\ oldK,newK:Commitment,Z:Evidence,\\ regrade:\mathrm{SemanticRegrade}\left(S\right),\\ \mathrm{Nonempty}\left(\mathrm{TargetLaunderingDecision}\left(S,oldK,newK,Z,regrade\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeRegrade/SemanticTargetLaunderingDecision.target_laundering_decision_nonempty (✓ std3). ∎

Source. Repository-derived.

Commentary.

For an arbitrary regrade semantic frame, commitment and evidence equality, each of the seven protected-coordinate equalities, and strict time comparison are decidable. No finite carrier, verdict equality, inhabited commitment type, or verdict-change premise is used.

Dependent protected-coordinate extensionality first supplies equality decision for the complete coordinate record. The frozen body-level characterization then decides the laundering predicate, and the returned Boolean carries its exact correctness equivalence.

The same module transcribes the standard interpreter from the existing prospective-commitment and regrade-report carriers and proves a named specialization through that interpreter. This discharges obligation 57.2-E from definition-escape-completion-theory atom generic-residual-18a12b09c5e901f1df86ba136d7ef48402e6fbabd170dd510c85c64d00c8a9f8.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeRegrade/SemanticTargetLaunderingDecision.target_laundering_decision_nonempty
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeRegrade/SemanticTargetLaunderingBundleElimination