Indexed Observation Closure Laws

Abstract

An arbitrary indexed universe of heterogeneous observations induces an extensive, monotone, idempotent closure with redundant added members.

Theorem 1.1 (Heterogeneous indexed observations generate a Galois closure).

$$\forall I\in Type,X\in Type,Y\in I\to Type,q\in \left(\forall i\in I,X\to Y\left(i\right)\right),Q\in \mathrm{Set}\left(I\right),Q2\in \mathrm{Set}\left(I\right),\mathrm{indexedObservationClosure}\left(q,Q\right)=\mathrm{invariantObservationIndices}\left(q,\mathrm{selectedObservationKernel}\left(q,Q\right)\right)\wedge \left(Q\subseteq \mathrm{indexedObservationClosure}\left(q,Q\right)\wedge \left(\left(Q\subseteq Q2\Rightarrow \mathrm{indexedObservationClosure}\left(q,Q\right)\subseteq \mathrm{indexedObservationClosure}\left(q,Q2\right)\right)\wedge \left(\mathrm{indexedObservationClosure}\left(q,\mathrm{indexedObservationClosure}\left(q,Q\right)\right)=\mathrm{indexedObservationClosure}\left(q,Q\right)\wedge \left(\forall i\in I,i\in \mathrm{indexedObservationClosure}\left(q,Q\right)\Rightarrow \mathrm{selectedObservationKernel}\left(q,\mathrm{insert}\left(i,Q\right)\right)=\mathrm{selectedObservationKernel}\left(q,Q\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The observation universe is an arbitrary index type. Each index may have its own output type, so the statement does not collapse the source language to one shared codomain or to all functions into it.

The selected kernel K records pairs identified by every chosen index, and I returns exactly the indices whose observations are invariant on a relation. The first public clause exposes Cl(Q) = I(K(Q)).

The remaining public clauses state extensivity, monotonicity, idempotence, and the unchanged-kernel criterion for every observation admitted by the closure.

References

• Truth anchor: D5/S3/ConceptDynamics/Closure/IndexedObservationClosureLaws.indexed_observation_closure_laws
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion