Protocol and Relation Closure Laws

Abstract

The canonical protocol and relation closures satisfy all three closure laws.

Theorem 1.1 (Both canonical closures are extensive, monotone, and idempotent).

$$\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),R\in \mathrm{Set}\left(X\times X\right),R2\in \mathrm{Set}\left(X\times X\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(R\subseteq \mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,R\right),\mathrm{val}\left(f\right)\right)\wedge \left(\left(R\subseteq R2\Rightarrow \mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,R\right),\mathrm{val}\left(f\right)\right)\subseteq \mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,R2\right),\mathrm{val}\left(f\right)\right)\right)\wedge \mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,\mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,R\right),\mathrm{val}\left(f\right)\right)\right),\mathrm{val}\left(f\right)\right)=\mathrm{jointKernel}\left(\lambda f:\mathrm{RelationInvariantReadouts}\left(O,R\right),\mathrm{val}\left(f\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

DefinitionClosure is the repository’s canonical protocol-family closure. The relation closure is constructed directly as the joint kernel of all RelationInvariantReadouts.

The public statement carries three protocol-side clauses followed by the corresponding three relation-side clauses: extensivity, monotonicity, and idempotence.

No new closure object is declared. The protocol laws reuse the frozen family theorem, while the relation laws follow from the canonical Galois primitives.

References

• Truth anchor: D5/S3/ConceptDynamics/Closure/ProtocolRelationClosureLaws.protocol_relation_closure_laws
• Dependency: D5/S3/ConceptDynamics/Closure/SourceClosureThreeLaws
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois