Escape Refinement Antitonicity

Abstract

Refining an observer family can only shrink its target defect and primitive escape.

Theorem 1.1 (Selected observer refinement shrinks target escape).

$$\begin{array}{r}\forall I:Type,X:Type,C:Type,Target:Type,\\ V:I\to Type,\\ S:\mathrm{Set}\left(I\right),S^{\prime }:\mathrm{Set}\left(I\right),\\ definitions:\forall i:I,\mathrm{Concept}\left(X,V(i)\right),\\ q:\mathrm{Concept}\left(X,C\right),target:\mathrm{Concept}\left(X,Target\right),\\ S\subseteq S^{\prime }\Rightarrow \mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{jointReadout}\left(\mathrm{restrict}\left(definitions,S^{\prime }\right)\right)\right),target\right)\subseteq \mathrm{defectRelation}\left(\mathrm{conceptJoin}\left(q,\mathrm{jointReadout}\left(\mathrm{restrict}\left(definitions,S\right)\right)\right),target\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscape/EscapeRefinementAntitone.escape_refinement_antitone (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary index, state, baseline, and target types, V is a dependent observer-codomain family and definitions supplies one concept at each index. The only order datum is S contained in S’.

Equality of the refined joint readout restricts pointwise to every index in S, while the target inequality is unchanged. Hence the defect relation for S’ is contained in the defect relation for S without finiteness, inhabitedness, or target-side premises.

Theorem 1.2 (Intersection-kernel primitive escape is antitone).

$$\begin{array}{r}\forall X:Type,InputOutput:Type,Output:Type,\\ Gamma:\mathrm{Set}\left(\mathrm{Concept}\left(X,InputOutput\right)\right),Delta:\mathrm{Set}\left(\mathrm{Concept}\left(X,InputOutput\right)\right),\\ Gamma\subseteq Delta\Rightarrow \{candidate:\mathrm{Concept}\left(X,Output\right)|\mathrm{PrimitiveEscape}\left(Delta,candidate\right)\}\subseteq \{candidate:\mathrm{Concept}\left(X,Output\right)|\mathrm{PrimitiveEscape}\left(Gamma,candidate\right)\}.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscape/EscapeRefinementAntitone.primitive_escape_refinement_antitone (✓ std3). ∎

Source. Repository-derived.

Commentary.

Gamma and Delta are homogeneous concept families with Gamma contained in Delta. PrimitiveEscape is the accepted complement of semantic closure, whose relation carrier is the intersection jointKernel.

The accepted jointKernel_antitone law sends every Delta-kernel pair to a Gamma-kernel pair. A candidate outside the larger semantic closure is therefore outside the smaller closure. This is the intersection-family form of the finite-window law above.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscape/EscapeRefinementAntitone.escape_refinement_antitone
• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscape/EscapeRefinementAntitone.primitive_escape_refinement_antitone
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionKernelGalois
• Dependency: D5/S3/ConceptDynamics/DefinitionEscape/FiniteCoverCounting