Complete productive-owner ledgers for schedule cursors

This module packages active, outside-window, and open-frame owner provenance into a cursor-level invariant.

structure IndexedGrammar.Aho.ScheduleOwnerLedger {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (window : ProductiveOwnerWindow parse) (cursor : ScheduleCursor g input) : Type

Complete cursor-level owner ledger, independent of any particular block-layout syntax.

• active : List (Fin (10 * input.length))
• outside : List (Fin (10 * input.length))
• right_eq : List.filterMap ScheduleAtom.indexOwner? cursor.right = self.active ++ self.outside
• outside_at (owner : Fin (10 * input.length)) : owner ∈ self.outside → OutsideProductiveWindow window owner
• frames : EventOwnedFrames parse window cursor.frameOwners
• prefixLedger : PrefixFrameLedger cursor

def IndexedGrammar.Aho.ScheduleOwnerLedger.root {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} (parse : g.NFParse g.initial [] input) : ScheduleOwnerLedger parse (ProductiveOwnerWindow.root parse) (initialScheduleCursor parse)

The canonical root cursor has no persistent, outside, or framed owners.

Equations

• IndexedGrammar.Aho.ScheduleOwnerLedger.root parse = { active := [], outside := [], right_eq := ⋯, outside_at := ⋯, frames := ⋯, prefixLedger := ⋯ }

theorem IndexedGrammar.Aho.ScheduleOwnerLedger.eventOwner_not_mem_indexOwners {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A : g.nt} {stack : List g.flag} {w : List T} {parse : g.NFParse A stack w} {window : ProductiveOwnerWindow parse} {cursor : ScheduleCursor g input} (ledger : ScheduleOwnerLedger parse window cursor) {blocks : List (List g.flag)} (activeLayout : EventOwnedLayout parse window blocks ledger.active) (hfocus : List.filterMap ScheduleAtom.indexOwner? [cursor.focus] = []) {d : ℕ} (hd : d ∈ parse.eventDepths) (hframeFresh : window.eventOwner d hd ∉ cursor.frameOwners) (hdiff : ∀ (i : Fin blocks.length), d ≠ blockEndpoint blocks i) : window.eventOwner d hd ∉ cursor.indexOwners

The complete schedule ledger specializes the generic whole-cursor freshness theorem.

def IndexedGrammar.Aho.ScheduleOwnerLedger.transport {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {A B : g.nt} {stack stack' : List g.flag} {w w' : List T} {parse : g.NFParse A stack w} {residual : g.NFParse B stack' w'} {window : ProductiveOwnerWindow parse} {old new : ScheduleCursor g input} (ledger : ScheduleOwnerLedger parse window old) (residualWindow : ProductiveOwnerWindow residual) (hright : List.filterMap ScheduleAtom.indexOwner? new.right = ledger.active ++ ledger.outside) (houtside : ∀ owner ∈ ledger.outside, OutsideProductiveWindow residualWindow owner) (hframes : EventOwnedFrames residual residualWindow new.frameOwners) (hprefix : PrefixFrameLedger new) : ScheduleOwnerLedger residual residualWindow new

Generic cursor reassembly after a parse/window transport.

Equations

• One or more equations did not get rendered due to their size.