Closed Coordinate Witness Bundle Characterization

Abstract

Closed nonempty coordinate witnesses exactly record changed protected coordinates.

Theorem 1.1 (Closed nonempty coordinate witnesses characterize record change).

$$\begin{array}{c}\forall TargetChain,Domain,Epsilon,Condition,Comparator,Baseline,WeightSpec:\mathrm{Type},\\ [\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)],\\ oldCoordinates,newCoordinates:\mathrm{ProtectedCoordinates}\left(TargetChain,Domain,Epsilon,Condition,Comparator,Baseline,WeightSpec\right),\\ \mathrm{HasClosedCoordinateWitnessBundle}\left(oldCoordinates,newCoordinates\right)⟺\\ oldCoordinates\ne newCoordinates.\end{array}$$

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

Source. Repository-derived.

Commentary.

CoordinateWitnessBundle records a finite set of changed labels and proves every registered dependent projection differs. Closed supplies the converse inclusion, while the existence predicate requires nonemptiness.

The reverse implication scans exactly the seven protected-coordinate labels using the supplied decidable equalities. If that scan were empty, frozen dependent extensionality would force the records equal.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeRegrade/CoordinateWitnessBundle.has_closed_coordinate_witness_bundle_iff_ne
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeRegrade/ProtectedCoordinateExtensionality