First Three Legacy Primitive Realizations

Abstract

The first three frozen statements are equivalent to their realization laws.

Definition 1.1 (Agenda power realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.agendaPowerRealization

Formalization. D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.agendaPowerRealization (✓ std3).

Source. Repository-derived.

Commentary.

The typed realization reads the sequential majority winner and decides ValidAgenda, with no point anchors.

Theorem 1.2 (Agenda power realization certificate).

$((\forall d es i re d : Fin (3), \exists a g e n d a : A g e n d a, (ValidAgenda (a g e n d a)) \land (sequentialWinner (maj or i t y P re f ers, a g e n d a) = d es i re d)) \land (\exists a g e n d aa g e n d a^{'} : A g e n d a, (ValidAgenda (a g e n d a)) \land (ValidAgenda (a g e n d a^{'})) \land (a g e n d a \neq = a g e n d a^{'}) \land (sequentialWinner (maj or i t y P re f ers, a g e n d a) \neq = sequentialWinner (maj or i t y P re f ers, a g e n d a^{'})))) ⟺ a g e n d a P o w er A re na . L a w a g e n d a P o w er R e a l i z a t i o n .$

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

Source. Repository-derived.

Commentary.

The certificate identifies the full frozen agenda-power proposition with agendaPowerArena.Law agendaPowerRealization.

Definition 1.3 (Residue realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.residueRealization

Formalization. D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.residueRealization (✓ std3).

Source. Repository-derived.

Commentary.

The typed realization uses residueReadout at every residue sensor and has no point anchors.

Theorem 1.4 (Adaptive residue realization certificate).

$((\forall s t a t e : R es i d u e St a t e, residueReadout (R es i d u e S e n sor . tw o, s t a t e) = f a l se ⟺ (s t a t e = zero St a t e) \lor (s t a t e = t e n St a t e)) \land (\forall s t a t e : R es i d u e St a t e, residueReadout (R es i d u e S e n sor . tw o, s t a t e) = t r u e ⟺ (s t a t e = f i f t ee n St a t e) \lor (s t a t e = tw e n t y O n e St a t e)) \land (\exists p ro t oco l : BinaryProtocol (R es i d u e St a t e, 2), (\forall hi s t ory : Fin (0) \to B oo l, p ro t oco l . q u es t i o n (⟨ 0, b y d ec i d e ⟩, hi s t ory) = residueReadout (R es i d u e S e n sor . tw o)) \land (\forall hi s t ory : Fin (1) \to B oo l, p ro t oco l . q u es t i o n (⟨ 1, b y d ec i d e ⟩, hi s t ory) = if (history (0), residueReadout (R es i d u e S e n sor . f i v e), residueReadout (R es i d u e S e n sor . t h ree))) \land (UsesReadoutFamily (res i d u e R e a d o u t, p ro t oco l)) \land (F u n c t i o n . I nj ec t i v e (p ro t oco l . t r an scr i pt))) \land (\forall se n sor : R es i d u e S e n sor, \neg F u n c t i o n . I nj ec t i v e (residueReadout (se n sor))) \land (\forall d e pt h : N a t, d e pt h < 2 \Rightarrow \neg ExactAtDepth (res i d u e R e a d o u t, d e pt h)) \land (res i d u e A d a pt i v eDe pt h = 2) \land (res i d u e St a t i cDe pt h = 3) \land (res i d u e A d a pt i v eDe pt h < res i d u e St a t i cDe pt h)) ⟺ res i d u e A re na . L a w res i d u e R e a l i z a t i o n .$

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

Source. Repository-derived.

Commentary.

The certificate identifies every clause of the frozen adaptive-residue proposition with residueArena.Law residueRealization.

Definition 1.5 (Spectrum realization).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.spectrumRealization

Formalization. D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.spectrumRealization (✓ std3).

Source. Repository-derived.

Commentary.

The typed realization reads SpectrumAtom.index at the sole readout and has no point anchors.

Theorem 1.6 (Spectrum index realization certificate).

$(F u n c t i o n . B ij ec t i v e (Sp ec t r u m A t o m . in d e x)) ⟺ s p ec t r u m A re na . L a w s p ec t r u m R e a l i z a t i o n .$

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

Source. Repository-derived.

Commentary.

The certificate identifies Function.Bijective SpectrumAtom.index with spectrumArena.Law spectrumRealization.

References

Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.agendaPowerRealization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.agenda_power_realization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.residueRealization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.spectrumRealization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.spectrum_atom_index_bijective_realization
Truth anchor: D5/S3/ConceptDynamics/InformationEscapeRealizations/FirstThreeRealizations.two_step_adaptive_residue_identification_realization
Dependency: D5/S3/ConceptDynamics/InformationEscapeArenas/FirstThreeArenas

Keyboard shortcuts

trureturing Blueprint

First Three Legacy Primitive Realizations

Abstract

References