Observation Closure Laws

Abstract

Observation closure has the three closure laws and adds no distinctions.

Theorem 1.1 (Observation closure is extensive, monotone, idempotent, and redundant).

$$\forall X\in Type,O\in Type,Q\in \mathrm{Set}\left(\mathrm{Concept}\left(X,O\right)\right),Q2\in \mathrm{Set}\left(\mathrm{Concept}\left(X,O\right)\right),Q\subseteq \mathrm{DefinitionClosure}\left(Q\right)\wedge \left(\left(Q\subseteq Q2\Rightarrow \mathrm{DefinitionClosure}\left(Q\right)\subseteq \mathrm{DefinitionClosure}\left(Q2\right)\right)\wedge \left(\mathrm{DefinitionClosure}\left(\mathrm{DefinitionClosure}\left(Q\right)\right)=\mathrm{DefinitionClosure}\left(Q\right)\wedge \left(\forall p\in \mathrm{Concept}\left(X,O\right),p\in \mathrm{DefinitionClosure}\left(Q\right)\Rightarrow \mathrm{jointKernel}\left(\lambda q:\mathrm{insert}\left(p,Q\right),\mathrm{val}\left(q\right)\right)=\mathrm{jointKernel}\left(\lambda q:Q,\mathrm{val}\left(q\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Closure/ObservationClosureLaws.observation_closure_laws (✓ std3). ∎

Source. Repository-derived.

Commentary.

DefinitionClosure is the canonical source-semantic closure constructed from the common observational kernel. The first three public clauses are its extensive, monotone, and idempotent laws.

The final public clause quantifies over every candidate in the closure. Inserting such a readout leaves the canonical joint kernel unchanged, so it cannot split a state pair left indistinguishable by the source family.

References

• Truth anchor: D5/S3/ConceptDynamics/Closure/ObservationClosureLaws.observation_closure_laws
• Dependency: D5/S3/ConceptDynamics/Closure/SourceClosureThreeLaws
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeLaws/SemanticClosureZeroGainCriterion