End State Omits Preempting Cause Realization

Abstract

Endpoint and active-cause readouts realize the five-class preemption kernel.

Definition 1.1 (Concrete preemption realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.endStateOmitsPreemptingCauseRealization

Formalization. D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.endStateOmitsPreemptingCauseRealization (✓ std3).

Source. Repository-derived.

Commentary.

The realization supplies endpoint, active-cause, ordered-preemption, and named-anchor data.

Theorem 1.2 (Preemption realization equivalence).

$IsOrderedPreemption (a T h e n B, s h oo t er A, s h oo t er B) \land IsOrderedPreemption (b T h e n A, s h oo t er B, s h oo t er A) \land endState (a T h e n B) = endState (b T h e n A) \land activeCause (a T h e n B) \neq = activeCause (b T h e n A) \land \neg \exists reco v er : B oo l \to Option (M ec hani s m), a c t i v e C a u se = reco v er \circ e n d St a t e ⟺ e n d St a t e O mi t s P ree m pt in g C a u se A re na . L a w e n d St a t e O mi t s P ree m pt in g C a u se R e a l i z a t i o n .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_realization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both directions encode or decode every clause of the frozen preemption statement.

Theorem 1.3 (Five kernel classes).

$(F in se t . u ni v . ima g e (λ t r a ce : P ree m pt i o n T r a ce, (endState (t r a ce), activeCause (t r a ce), decide (IsOrderedPreemption (t r a ce, s h oo t er A, s h oo t er B)), decide (IsOrderedPreemption (t r a ce, s h oo t er B, s h oo t er A)), decide (t r a ce = a T h e n B), decide (t r a ce = b T h e n A)))) . c a r d = 5.$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_partition_count (✓ std3). ∎

Source. Repository-derived.

Commentary.

The concrete six-component image of all preemption traces has five elements.

Theorem 1.4 (Private trace separation).

$\neg e n d St a t e O mi t s P ree m pt in g C a u se R e a l i z a t i o n . t o P r imi t i v e B u n d l e . a g rees a T h e n B b T h e n A .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_private_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

The compiled primitive bundle separates the two named traces.

References

Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.endStateOmitsPreemptingCauseRealization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_partition_count
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_private_pair
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/EndStateOmitsPreemptingCause.end_state_omits_preempting_cause_realization
Dependency: D5/S3/ConceptDynamics/InformationEscapeArenas/EndStateOmitsPreemptingCause

Keyboard shortcuts

trureturing Blueprint

End State Omits Preempting Cause Realization

Abstract

References