One-Step Closure Fivefold Equivalence

Abstract

One-step kernel closure is equivalent to complete behavioral closure, exact descent, and absence of carry.

Theorem 1.1 (Five closure criteria are equivalent).

$$\begin{array}{c}\forall X,B:\mathrm{Type},\\ q:X\to B,F:X\to X,\\ \mathrm{ListTFAE}\left([\mathrm{depthZeroKernel}\left(q\right)=\mathrm{depthOneKernel}\left(q,F\right),\mathrm{InterfaceCongruence}\left(q,F\right),Setoid.kerq=Setoid.ker(\mathrm{completeItinerary}\left(F,q\right)),\mathrm{EffectiveDescent}\left(q,F\right),\forall x,y:X,\neg \mathrm{IsCarryWitness}\left(q,F,q,x,y\right)]\right)\wedge \\ ((\exists x,y:X,\mathrm{IsCarryWitness}\left(q,F,q,x,y\right))⟺\mathrm{depthOneKernel}\left(q,F\right)<\mathrm{depthZeroKernel}\left(q\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Dialectics/OneStepClosureFivefoldEquivalence.one_step_closure_fivefold_equivalence (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any state type, readout, and deterministic update, equality of the depth-zero and depth-one kernels is equivalent to forward fiber invariance, equality with the complete-itinerary kernel, unique effective descent on the realized image, and absence of carry.

The final clause identifies the complementary event: a carry witness exists exactly when the depth-one kernel is a strict refinement of the depth-zero kernel. No finiteness or nonemptiness assumption is used.

References

• Truth anchor: D5/S3/ConceptDynamics/Dialectics/OneStepClosureFivefoldEquivalence.one_step_closure_fivefold_equivalence
• Dependency: D5/S3/ConceptDynamics/Dialectics/DeterministicInterfaceEquivalence
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion