The compressed-block budget along a consumption route

Unary push/pop stretches of a chosen consumption route may be compressed into one index block. Crossing a binary node ends the current stretch and starts another one. Thus the number of maximal binary-free chunks is one plus the number of binary barriers on the route.

barrierOwners already charges every barrier to a distinct terminal in the off-route child. The missing final charge is a terminal in the child followed by the route. Adding this owner makes the bound sharp: the number of chunks, rather than merely the number of barriers, is at most the terminal yield length.

def IndexedGrammar.NFParse.ConsumeRoute.followedOwner {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} : ConsumeRoute g p k → Fin w.length

A terminal position that stays inside the branch followed by a consumption route.

Equations

• route.binaryLeft.followedOwner = IndexedGrammar.NFParse.ConsumeRoute.embedLeft u v route.followedOwner
• route.binaryRight.followedOwner = IndexedGrammar.NFParse.ConsumeRoute.embedRight u v route.followedOwner
• IndexedGrammar.NFParse.ConsumeRoute.popHere.followedOwner = ⟨0, ⋯⟩
• route.popTail.followedOwner = route.followedOwner
• route.push.followedOwner = route.followedOwner

theorem IndexedGrammar.NFParse.ConsumeRoute.followedOwner_not_mem_barrierOwners {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.followedOwner ∉ route.barrierOwners

The on-route terminal owner is disjoint from every off-route barrier owner.

theorem IndexedGrammar.NFParse.ConsumeRoute.followedOwner_cons_barrierOwners_nodup {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : (route.followedOwner :: route.barrierOwners).Nodup

The terminal followed by the route together with all off-route charges is duplicate-free.

theorem IndexedGrammar.NFParse.ConsumeRoute.barrierOwners_length_add_one_le {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.barrierOwners.length + 1 ≤ w.length

There is room for both every binary barrier and the final followed branch in the yield.

def IndexedGrammar.NFParse.ConsumeRoute.noBinaryChunkCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} : ConsumeRoute g p k → ℕ

Number of maximal binary-free chunks on a consumption route. Unary constructors stay in the current chunk; each binary constructor starts exactly one further chunk.

Equations

• route.binaryLeft.noBinaryChunkCount = route.noBinaryChunkCount + 1
• route.binaryRight.noBinaryChunkCount = route.noBinaryChunkCount + 1
• IndexedGrammar.NFParse.ConsumeRoute.popHere.noBinaryChunkCount = 1
• route.popTail.noBinaryChunkCount = route.noBinaryChunkCount
• route.push.noBinaryChunkCount = route.noBinaryChunkCount

theorem IndexedGrammar.NFParse.ConsumeRoute.noBinaryChunkCount_eq_barrierOwners_length_add_one {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.noBinaryChunkCount = route.barrierOwners.length + 1

Chunk count is precisely one plus the existing barrier count.

theorem IndexedGrammar.NFParse.ConsumeRoute.noBinary_iff_chunkCount_eq_one {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.NoBinary ↔ route.noBinaryChunkCount = 1

A route is one maximal chunk exactly when it is binary-free.

theorem IndexedGrammar.NFParse.ConsumeRoute.noBinaryChunkCount_le_yield_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) : route.noBinaryChunkCount ≤ w.length

The number of compressed blocks needed by the maximal binary-free decomposition is bounded by the terminal yield. This is the index-payload inequality needed by ScheduleInvariant.

Prefix truncation of a chosen consumption route

@[irreducible]

def IndexedGrammar.NFParse.ConsumeRoute.truncate {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) (j : ℕ) (hjk : j ≤ k) : ConsumeRoute g p j

Follow the same branch choices only as far as a shallower inherited occurrence. This is a structural truncation, not a fresh classical choice of route, so it preserves the absence of binary barriers.

Equations

• One or more equations did not get rendered due to their size.
• inner.binaryLeft.truncate j hjk = (inner.truncate j hjk).binaryLeft
• inner.binaryRight.truncate j hjk = (inner.truncate j hjk).binaryRight
• inner.push.truncate j hjk = (inner.truncate (j + 1) ⋯).push

theorem IndexedGrammar.NFParse.ConsumeRoute.truncate_noBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) (hroute : route.NoBinary) (j : ℕ) (hjk : j ≤ k) : (route.truncate j hjk).NoBinary

Truncating a binary-free route to a shallower occurrence remains binary-free.

theorem IndexedGrammar.NFParse.ConsumeRoute.barrierOwners_truncate_prefix {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) (j : ℕ) (hjk : j ≤ k) : (route.truncate j hjk).barrierOwners <+: route.barrierOwners

Truncation keeps an initial segment of the original route's barrier charges. In particular, it neither invents a binary barrier nor changes the owner assigned to a barrier it retains.

theorem IndexedGrammar.NFParse.ConsumeRoute.noBinaryChunkCount_truncate_le {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : ConsumeRoute g p k) (j : ℕ) (hjk : j ≤ k) : (route.truncate j hjk).noBinaryChunkCount ≤ route.noBinaryChunkCount

Consequently truncation cannot increase the number of maximal binary-free chunks.

theorem IndexedGrammar.NFParse.ConsumeRoute.barrierOwners_ne_nil_of_truncate_not_noBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k j : ℕ} (route : ConsumeRoute g p k) (hjk : j ≤ k) (hunsafe : ¬(route.truncate j hjk).NoBinary) : route.barrierOwners ≠ []

If a structural truncation is unsafe for unary compression, the original route has at least one binary-barrier owner.

theorem IndexedGrammar.NFParse.ConsumeRoute.two_le_noBinaryChunkCount_of_truncate_not_noBinary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k j : ℕ} (route : ConsumeRoute g p k) (hjk : j ≤ k) (hunsafe : ¬(route.truncate j hjk).NoBinary) : 2 ≤ route.noBinaryChunkCount

Equivalently, an unsafe truncation certifies that the original route needs at least two maximal binary-free chunks.

def IndexedGrammar.NFParse.eventDepths {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} : g.NFParse A stack w → Finset ℕ

Stack depths at which a productive parse event can end a compressed unary block.

Terminal leaves and binary forks contribute the current depth. A pop shifts every deeper event one position away from the root, while a push removes the freshly pushed position.

Equations

• (IndexedGrammar.NFParse.binary hr hlhs hc hrhs left right).eventDepths = insert 0 (left.eventDepths ∪ right.eventDepths)
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).eventDepths = Finset.image Nat.succ rest.eventDepths
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).eventDepths = Finset.image Nat.pred rest.eventDepths
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).eventDepths = {0}

def IndexedGrammar.Aho.ScheduleTask.embedYieldOwner {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) : Fin task.yield.length → Fin input.length

Embed a terminal position of a pending task's yield into the complete input word.

Equations

• task.embedYieldOwner owner = ⟨task.pre.length + ↑owner, ⋯⟩

theorem IndexedGrammar.Aho.ScheduleTask.embedYieldOwner_injective {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) : Function.Injective task.embedYieldOwner

theorem IndexedGrammar.Aho.ScheduleTask.embedYieldOwner_zero_eq_owner {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) : task.embedYieldOwner ⟨0, ⋯⟩ = task.owner

The task's ordinary owner is the embedding of the first terminal in its yield.

def IndexedGrammar.Aho.ScheduleTask.routeBlockOwners {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) {k : ℕ} (route : NFParse.ConsumeRoute g task.parse k) : List (Fin input.length)

Absolute input owners for all compressed blocks in the maximal binary-free decomposition of a chosen consumption route belonging to this task.

Equations

• task.routeBlockOwners route = List.map task.embedYieldOwner (route.followedOwner :: route.barrierOwners)

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_nodup {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) {k : ℕ} (route : NFParse.ConsumeRoute g task.parse k) : (task.routeBlockOwners route).Nodup

Block owners belonging to one task are pairwise distinct.

@[simp]

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_length {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) {k : ℕ} (route : NFParse.ConsumeRoute g task.parse k) : (task.routeBlockOwners route).length = route.noBinaryChunkCount

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_length_le_yield {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) {k : ℕ} (route : NFParse.ConsumeRoute g task.parse k) : (task.routeBlockOwners route).length ≤ task.yield.length

A task's compressed blocks fit within its own yield interval.

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_length_le_input {T : Type} {g : IndexedGrammar T} {input : List T} (task : ScheduleTask g input) {k : ℕ} (route : NFParse.ConsumeRoute g task.parse k) : (task.routeBlockOwners route).length ≤ input.length

In particular, the local block-owner count satisfies the global input-length budget used by ScheduleInvariant.indexCount_le.

def IndexedGrammar.Aho.ScheduleTask.YieldBefore {T : Type} {g : IndexedGrammar T} {input : List T} (left right : ScheduleTask g input) : Prop

The yield interval of left lies completely before the yield interval of right.

Equations

• left.YieldBefore right = (left.pre.length + left.yield.length ≤ right.pre.length)

theorem IndexedGrammar.Aho.ScheduleTask.embedYieldOwner_ne_of_yieldBefore {T : Type} {g : IndexedGrammar T} {input : List T} {left right : ScheduleTask g input} (hbefore : left.YieldBefore right) (i : Fin left.yield.length) (j : Fin right.yield.length) : left.embedYieldOwner i ≠ right.embedYieldOwner j

Owners embedded from disjointly ordered task intervals cannot coincide.

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_disjoint_of_yieldBefore {T : Type} {g : IndexedGrammar T} {input : List T} {left right : ScheduleTask g input} (hbefore : left.YieldBefore right) {i j : ℕ} (leftRoute : NFParse.ConsumeRoute g left.parse i) (rightRoute : NFParse.ConsumeRoute g right.parse j) : (left.routeBlockOwners leftRoute).Disjoint (right.routeBlockOwners rightRoute)

Compressed-block owner lists from disjoint pending-task intervals are disjoint.

theorem IndexedGrammar.Aho.ScheduleTask.routeBlockOwners_append_nodup_of_yieldBefore {T : Type} {g : IndexedGrammar T} {input : List T} {left right : ScheduleTask g input} (hbefore : left.YieldBefore right) {i j : ℕ} (leftRoute : NFParse.ConsumeRoute g left.parse i) (rightRoute : NFParse.ConsumeRoute g right.parse j) : (left.routeBlockOwners leftRoute ++ right.routeBlockOwners rightRoute).Nodup

Consequently concatenating the compressed blocks of two ordered task intervals preserves the global no-duplicate ownership invariant.

Persistent ownership of inherited block partitions

structure IndexedGrammar.Aho.BlockOwnership (N : ℕ) {X : Type} (blocks : List X) : Type

A block list together with one pairwise-distinct owner in an ambient finite budget for each block. The carrier is independent of how a child refines its local event cuts, so ancestor owners can persist unchanged throughout the runner.

• owners : List (Fin N)
• owners_length : self.owners.length = blocks.length
• owners_nodup : self.owners.Nodup

def IndexedGrammar.Aho.BlockOwnership.nil (N : ℕ) {X : Type} : BlockOwnership N []

Equations

• IndexedGrammar.Aho.BlockOwnership.nil N = { owners := [], owners_length := ⋯, owners_nodup := ⋯ }

def IndexedGrammar.Aho.BlockOwnership.cons {N : ℕ} {X : Type} {blocks : List X} (block : X) (owner : Fin N) (ownership : BlockOwnership N blocks) (hfresh : owner ∉ ownership.owners) : BlockOwnership N (block :: blocks)

Add a fresh owner in front of an existing aligned block list.

Equations

• IndexedGrammar.Aho.BlockOwnership.cons block owner ownership hfresh = { owners := owner :: ownership.owners, owners_length := ⋯, owners_nodup := ⋯ }

def IndexedGrammar.Aho.BlockOwnership.take {N : ℕ} {X : Type} {blocks : List X} (n : ℕ) (ownership : BlockOwnership N blocks) : BlockOwnership N (List.take n blocks)

Retain ownership for the first n blocks.

Equations

• IndexedGrammar.Aho.BlockOwnership.take n ownership = { owners := List.take n ownership.owners, owners_length := ⋯, owners_nodup := ⋯ }

def IndexedGrammar.Aho.BlockOwnership.drop {N : ℕ} {X : Type} {blocks : List X} (n : ℕ) (ownership : BlockOwnership N blocks) : BlockOwnership N (List.drop n blocks)

Retain ownership for the blocks after the first n.

Equations

• IndexedGrammar.Aho.BlockOwnership.drop n ownership = { owners := List.drop n ownership.owners, owners_length := ⋯, owners_nodup := ⋯ }

def IndexedGrammar.Aho.BlockOwnership.Disjoint {N : ℕ} {X Y : Type} {leftBlocks : List X} {rightBlocks : List Y} (left : BlockOwnership N leftBlocks) (right : BlockOwnership N rightBlocks) : Prop

Ownership carriers are disjoint when their concrete owner lists are disjoint.

Equations

• left.Disjoint right = left.owners.Disjoint right.owners

theorem IndexedGrammar.Aho.BlockOwnership.disjoint_comm {N : ℕ} {X Y : Type} {leftBlocks : List X} {rightBlocks : List Y} {left : BlockOwnership N leftBlocks} {right : BlockOwnership N rightBlocks} : left.Disjoint right ↔ right.Disjoint left

def IndexedGrammar.Aho.BlockOwnership.append {N : ℕ} {X : Type} {leftBlocks rightBlocks : List X} (left : BlockOwnership N leftBlocks) (right : BlockOwnership N rightBlocks) (hdisjoint : left.Disjoint right) : BlockOwnership N (leftBlocks ++ rightBlocks)

Concatenate two aligned carriers whose owner sets are disjoint.

Equations

• left.append right hdisjoint = { owners := left.owners ++ right.owners, owners_length := ⋯, owners_nodup := ⋯ }

theorem IndexedGrammar.Aho.BlockOwnership.disjoint_take_drop {N : ℕ} {X : Type} {blocks : List X} (n : ℕ) (ownership : BlockOwnership N blocks) : (take n ownership).Disjoint (drop n ownership)

The prefix and suffix inherited from one carrier have disjoint owner sets.

theorem IndexedGrammar.Aho.BlockOwnership.blocks_length_le {N : ℕ} {X : Type} {blocks : List X} (ownership : BlockOwnership N blocks) : blocks.length ≤ N

Distinct finite owners give the required ambient block-count bound.

Transient-index accounting

theorem IndexedGrammar.Aho.framed_cell_count_le_eight_mul_of_index_add_one_le_two_mul {tasks indices frames n : ℕ} (htasks : tasks ≤ n) (hindices : indices + 1 ≤ 2 * n) (hframes : frames ≤ indices) (hn : 0 < n) : tasks + indices + 2 * frames + 2 ≤ 8 * n

Arithmetic form used by the transient compressed-token scheduler. Tasks still inject into the n terminal positions. Persistent indices together with the one currently transient index fit in two copies of those positions, and every open frame is charged to a persistent index.

Accounting carried by every compressed-runner edge

def IndexedGrammar.Aho.WorkSym.isTaskPayload {T : Type} {g : IndexedGrammar T} : WorkSym g → Bool

Does a physical work symbol carry one pending-task or emitted-terminal payload?

Equations

• (IndexedGrammar.Aho.WorkSym.terminal a).isTaskPayload = true
• (IndexedGrammar.Aho.WorkSym.plain a).isTaskPayload = true
• (IndexedGrammar.Aho.WorkSym.live a).isTaskPayload = true
• x✝.isTaskPayload = false

def IndexedGrammar.Aho.WorkSym.isClose {T : Type} {g : IndexedGrammar T} : WorkSym g → Bool

Does a physical work symbol close one currently open scheduler frame?

Equations

• IndexedGrammar.Aho.WorkSym.close.isClose = true
• x✝.isClose = false

def IndexedGrammar.Aho.workTaskCount {T : Type} {g : IndexedGrammar T} (c : Config g) : ℕ

Physical task/terminal payload count of one concrete configuration.

Equations

• IndexedGrammar.Aho.workTaskCount c = List.countP IndexedGrammar.Aho.WorkSym.isTaskPayload c.work.word

def IndexedGrammar.Aho.workIndexCount {T : Type} {g : IndexedGrammar T} (c : Config g) : ℕ

Physical compressed-index count of one concrete configuration.

Equations

• IndexedGrammar.Aho.workIndexCount c = List.countP IndexedGrammar.Aho.WorkSym.isIndex c.work.word

def IndexedGrammar.Aho.workFrameCount {T : Type} {g : IndexedGrammar T} (c : Config g) : ℕ

Physical open-frame count, measured by closing delimiters.

Equations

• IndexedGrammar.Aho.workFrameCount c = List.countP IndexedGrammar.Aho.WorkSym.isClose c.work.word

Exact count formulas for runner configurations

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_config_mk {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (left : List (WorkSym g)) (focus : WorkSym g) (right : List (WorkSym g)) : workTaskCount { inputPos := inputPos, work := { left := left, focus := focus, right := right } } = List.countP WorkSym.isTaskPayload left + List.countP WorkSym.isTaskPayload [focus] + List.countP WorkSym.isTaskPayload right

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_config_mk {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (left : List (WorkSym g)) (focus : WorkSym g) (right : List (WorkSym g)) : workIndexCount { inputPos := inputPos, work := { left := left, focus := focus, right := right } } = List.countP WorkSym.isIndex left + List.countP WorkSym.isIndex [focus] + List.countP WorkSym.isIndex right

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_config_mk {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (left : List (WorkSym g)) (focus : WorkSym g) (right : List (WorkSym g)) : workFrameCount { inputPos := inputPos, work := { left := left, focus := focus, right := right } } = List.countP WorkSym.isClose left + List.countP WorkSym.isClose [focus] + List.countP WorkSym.isClose right

theorem IndexedGrammar.Aho.countP_markProductivePrefix_of_index_mark_invariant {T : Type} {g : IndexedGrammar T} (predicate : WorkSym g → Bool) (hmark : ∀ (R : CFlag g) (d : IndexMark), predicate (WorkSym.index R d.markUsed) = predicate (WorkSym.index R d)) (xs : List (WorkSym g)) : List.countP predicate (markProductivePrefix xs) = List.countP predicate xs

Marking the rightmost index changes no count computed from a mark-insensitive predicate.

@[simp]

theorem IndexedGrammar.Aho.countP_isTaskPayload_markProductivePrefix {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : List.countP WorkSym.isTaskPayload (markProductivePrefix xs) = List.countP WorkSym.isTaskPayload xs

@[simp]

theorem IndexedGrammar.Aho.countP_isIndex_markProductivePrefix {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : List.countP WorkSym.isIndex (markProductivePrefix xs) = List.countP WorkSym.isIndex xs

@[simp]

theorem IndexedGrammar.Aho.countP_isClose_markProductivePrefix {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : List.countP WorkSym.isClose (markProductivePrefix xs) = List.countP WorkSym.isClose xs

@[simp]

theorem IndexedGrammar.Aho.markProductivePrefix_length {T : Type} {g : IndexedGrammar T} (xs : List (WorkSym g)) : (markProductivePrefix xs).length = xs.length

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_wordConfig {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha word : List (WorkSym g)) : workTaskCount (wordConfig g inputPos alpha word) = List.countP WorkSym.isTaskPayload alpha + List.countP WorkSym.isTaskPayload word

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_wordConfig {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha word : List (WorkSym g)) : workIndexCount (wordConfig g inputPos alpha word) = List.countP WorkSym.isIndex alpha + List.countP WorkSym.isIndex word

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_wordConfig {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha word : List (WorkSym g)) : workFrameCount (wordConfig g inputPos alpha word) = List.countP WorkSym.isClose alpha + List.countP WorkSym.isClose word

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_active_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } = List.countP WorkSym.isTaskPayload alpha + List.countP WorkSym.isTaskPayload beta + 1

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_active_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } = List.countP WorkSym.isIndex alpha + List.countP WorkSym.isIndex beta

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_active_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.plain A, right := beta } } = List.countP WorkSym.isClose alpha + List.countP WorkSym.isClose beta

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_active_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta } } = List.countP WorkSym.isTaskPayload alpha + List.countP WorkSym.isTaskPayload beta + 1

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_active_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta } } = List.countP WorkSym.isIndex alpha + List.countP WorkSym.isIndex beta

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_active_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta : List (WorkSym g)) (A : g.nt) : workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := WorkSym.live A, right := beta } } = List.countP WorkSym.isClose alpha + List.countP WorkSym.isClose beta

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_popOpen_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.plain B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isTaskPayload alpha + List.countP WorkSym.isTaskPayload beta + List.countP WorkSym.isTaskPayload gamma + 1

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_popOpen_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.plain B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isIndex alpha + List.countP WorkSym.isIndex beta + List.countP WorkSym.isIndex gamma + 1

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_popOpen_plain {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.plain B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isClose alpha + List.countP WorkSym.isClose beta + List.countP WorkSym.isClose gamma + 1

@[simp]

theorem IndexedGrammar.Aho.workTaskCount_popOpen_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.live B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isTaskPayload alpha + List.countP WorkSym.isTaskPayload beta + List.countP WorkSym.isTaskPayload gamma + 1

@[simp]

theorem IndexedGrammar.Aho.workIndexCount_popOpen_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.live B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isIndex alpha + List.countP WorkSym.isIndex beta + List.countP WorkSym.isIndex gamma + 1

@[simp]

theorem IndexedGrammar.Aho.workFrameCount_popOpen_live {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (R : CFlag g) (d : IndexMark) (B : g.nt) : workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar] ++ beta ++ [WorkSym.index R d.markUsed, WorkSym.dollar], focus := WorkSym.live B, right := WorkSym.close :: gamma } } = List.countP WorkSym.isClose alpha + List.countP WorkSym.isClose beta + List.countP WorkSym.isClose gamma + 1

theorem IndexedGrammar.Aho.workTaskCount_returnFrame_eq {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (Z : WorkSym g) : workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } } = workTaskCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } }

Returning a frame preserves task and index counts and removes exactly its closing marker.

theorem IndexedGrammar.Aho.workIndexCount_returnFrame_eq {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (Z : WorkSym g) : workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } } = workIndexCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } }

theorem IndexedGrammar.Aho.workFrameCount_returnFrame_eq_add_one {T : Type} {g : IndexedGrammar T} (inputPos : ℕ) (alpha beta gamma : List (WorkSym g)) (Z : WorkSym g) : workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar, Z] ++ beta ++ [WorkSym.dollar], focus := WorkSym.close, right := gamma } } = workFrameCount { inputPos := inputPos, work := { left := alpha ++ [WorkSym.dollar], focus := Z, right := beta ++ gamma } } + 1

structure IndexedGrammar.Aho.CompressedAccounting {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (c : Config g) : Prop

Accounting for one concrete compressed-runner configuration. Every count is computed from the physical word itself; event-depth invariants prove the count bounds, while shape_bound records the delimiter layout.

• taskCount_le : workTaskCount c ≤ input.length
• indexCount_add_one_le : workIndexCount c + 1 ≤ 2 * input.length
• frameCount_le_indexCount : workFrameCount c ≤ workIndexCount c
• shape_bound : c.work.word.length ≤ workTaskCount c + workIndexCount c + 2 * workFrameCount c + 2

theorem IndexedGrammar.Aho.CompressedAccounting.of_physical_bounds {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c : Config g} (htasks : workTaskCount c ≤ input.length) (hindices : workIndexCount c + 1 ≤ 2 * input.length) (hframes : workFrameCount c ≤ workIndexCount c) (hshape : c.work.word.length ≤ workTaskCount c + workIndexCount c + 2 * workFrameCount c + 2) : CompressedAccounting g input c

Package explicit bounds on the three physical count functions.

theorem IndexedGrammar.Aho.CompressedAccounting.within {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c : Config g} (accounting : CompressedAccounting g input c) (hinput : 0 < input.length) : Config.Within (15 * input.length) c

The accounting inequalities turn a local witness into the physical work-tape bound.

theorem IndexedGrammar.Aho.initialConfig_compressedAccounting {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (hinput : 0 < input.length) : CompressedAccounting g input (initialConfig g)

The initial work word has one task payload and no indices or frames.

theorem IndexedGrammar.Aho.finalConfig_compressedAccounting {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (hinput : 0 < input.length) : CompressedAccounting g input (finalConfig g input.length)

The final work word has no task, index, or frame payload.

def IndexedGrammar.Aho.CompressedReaches {T : Type} (g : IndexedGrammar T) [Fintype g.nt] (input : List T) (c c' : Config g) : Prop

Composite reachability with an event-depth accounting witness on the initial configuration and on both endpoints of every edge. This shape composes at exact Config endpoints and prevents a runner proof from silently passing through an unbounded intermediate configuration.

Equations

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

theorem IndexedGrammar.Aho.CompressedReaches.refl {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c : Config g} (hc : CompressedAccounting g input c) : CompressedReaches g input c c

theorem IndexedGrammar.Aho.CompressedReaches.single {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c c' : Config g} (hc : CompressedAccounting g input c) (hstep : CompositeStep g input c c') (hc' : CompressedAccounting g input c') : CompressedReaches g input c c'

theorem IndexedGrammar.Aho.CompressedReaches.trans {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c₁ c₂ c₃ : Config g} (h₁₂ : CompressedReaches g input c₁ c₂) (h₂₃ : CompressedReaches g input c₂ c₃) : CompressedReaches g input c₁ c₃

theorem IndexedGrammar.Aho.CompressedReaches.target_accounting {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c c' : Config g} (run : CompressedReaches g input c c') : CompressedAccounting g input c'

The last configuration of an accounted trace retains an accounting witness, including in the reflexive case.

theorem IndexedGrammar.Aho.CompressedReaches.toReflTransGen {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c c' : Config g} (run : CompressedReaches g input c c') : Relation.ReflTransGen (CompositeStep g input) c c'

Forget accounting annotations and retain ordinary composite reachability.

theorem IndexedGrammar.Aho.CompressedReaches.toBoundedReaches {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {input : List T} {c c' : Config g} (hinput : 0 < input.length) (run : CompressedReaches g input c c') : BoundedReaches g input (15 * input.length) c c'

Every accounted compressed trace is a bounded composite trace at the desired linear bound.

Binary-free block continuations

theorem IndexedGrammar.Aho.consumeRoute_popContinuation_noBinary_with_consumption {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} {p : g.NFParse A stack w} {k : ℕ} (route : NFParse.ConsumeRoute g p k) (hroute : route.NoBinary) : ∃ (Y : g.nt) (suffix : List g.flag) (rest : g.NFParse Y suffix w), suffix = List.drop (k + 1) stack ∧ PopPath g A (List.take (k + 1) stack) Y ∧ rest.nodeCount < p.nodeCount ∧ (∀ (j : ℕ), rest.ConsumesAt j ↔ p.ConsumesAt (k + 1 + j)) ∧ ∀ (d : ℕ), d ∈ rest.eventDepths ↔ k + 1 + d ∈ p.eventDepths

Strengthening of consumeRoute_popContinuation_noBinary: after the whole compressed block through occurrence k is popped, consumption by the residual parse at position j is exactly consumption by the original parse at position k + 1 + j. Thus an atomic multi-flag pop can continue against lower compressed blocks without losing the live/plain boundary information.

Visible prefixes represented by compressed blocks

inductive IndexedGrammar.Aho.BlockLayout {T : Type} (g : IndexedGrammar T) [Fintype g.nt] : List g.flag → List (List g.flag) → List (WorkSym g) → List (WorkSym g) → Prop

A compressed visible-stack layout. flags is partitioned by the nonempty lists in blocks; every block is represented by one relation token which denotes exactly that concrete flag list. Gaps may contain ordinary control symbols (including close) but neither another index nor $. The third and fourth word indices differ only by marking every selected token used.

• nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (tail : List (WorkSym g)) : BlockLayout g [] [] tail tail
• cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {block flags : List g.flag} {blocks : List (List g.flag)} {beta tail tail' : List (WorkSym g)} {R : CFlag g} {d : IndexMark} (block_ne : block ≠ []) (denotes : CFlag.Denotes g block R) (indexFree : IndexFree beta) (dollarFree : DollarFree beta) (later : flags ≠ [] → d.later = true) (rest : BlockLayout g flags blocks tail tail') : BlockLayout g (block ++ flags) (block :: blocks) (beta ++ WorkSym.index R d :: tail) (beta ++ WorkSym.index R d.markUsed :: tail')

@[simp]

theorem IndexedGrammar.Aho.BlockLayout.IndexMark.markUsed_idem (d : IndexMark) : d.markUsed.markUsed = d.markUsed

@[simp]

theorem IndexedGrammar.Aho.BlockLayout.IndexMark.markUsed_later (d : IndexMark) : d.markUsed.later = d.later

theorem IndexedGrammar.Aho.BlockLayout.flags_eq_flatten {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) : flags = blocks.flatten

The concrete visible prefix is exactly the flattening of its block partition.

theorem IndexedGrammar.Aho.BlockLayout.blocks_nonempty {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) (block : List g.flag) : block ∈ blocks → block ≠ []

Every member of the partition is a nonempty concrete flag block.

theorem IndexedGrammar.Aho.BlockLayout.head_denotation {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {block flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags (block :: blocks) word used) : ∃ (beta : List (WorkSym g)) (tail : List (WorkSym g)) (tail' : List (WorkSym g)) (R : CFlag g) (d : IndexMark), CFlag.Denotes g block R ∧ block ≠ [] ∧ IndexFree beta ∧ DollarFree beta ∧ word = beta ++ WorkSym.index R d :: tail ∧ used = beta ++ WorkSym.index R d.markUsed :: tail'

Every relation stored by the layout retains a concrete denotation witness.

theorem IndexedGrammar.Aho.BlockLayout.idempotent {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) : BlockLayout g flags blocks used used

Re-selecting an all-used block layout is physically idempotent.

theorem IndexedGrammar.Aho.BlockLayout.prepend {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (pref : List (WorkSym g)) (hindex : IndexFree pref) (hdollar : DollarFree pref) (layout : BlockLayout g flags blocks word used) : BlockLayout g flags blocks (pref ++ word) (pref ++ used)

Insert an ordinary control prefix into the gap before the first selected block.

theorem IndexedGrammar.Aho.BlockLayout.blocks_eq_nil_of_flags_eq_nil {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) (hflags : flags = []) : blocks = []

A layout with no concrete flags has no blocks. The nonempty-block invariant is essential: without it flatten blocks = [] would not force blocks = [].

theorem IndexedGrammar.Aho.BlockLayout.take_flatten_take {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) (n : ℕ) : List.take (List.take n blocks).flatten.length flags = (List.take n blocks).flatten

Taking the concrete number of flags covered by the first n blocks ends exactly at their physical block boundary.

theorem IndexedGrammar.Aho.BlockLayout.splitTake {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (n : ℕ) (layout : BlockLayout g flags blocks word used) : ∃ (middle : List (WorkSym g)), BlockLayout g (List.take n blocks).flatten (List.take n blocks) word middle ∧ BlockLayout g flags blocks middle used

Restrict a layout to its first n whole blocks. The remaining selected tokens become part of the intermediate word. Unlike a flagwise split, this operation can never cut through the concrete denotation of one compressed relation.

structure IndexedGrammar.Aho.BlockLayout.Boundary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (blocks : List (List g.flag)) (flagCount : ℕ) : Type

A concrete flag position is aligned to the compressed layout when it is the total length of some whole-block prefix. The explicit block count is the physical index-token budget at that boundary.

• blockCount : ℕ
• blockCount_le : self.blockCount ≤ blocks.length
• flagCount_eq : flagCount = (List.take self.blockCount blocks).flatten.length

def IndexedGrammar.Aho.BlockLayout.Boundary.ofBlockCount {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (blocks : List (List g.flag)) (blockCount : ℕ) (h : blockCount ≤ blocks.length) : Boundary blocks (List.take blockCount blocks).flatten.length

Every prefix measured in whole blocks determines an aligned concrete boundary.

Equations

• IndexedGrammar.Aho.BlockLayout.Boundary.ofBlockCount blocks blockCount h = { blockCount := blockCount, blockCount_le := h, flagCount_eq := ⋯ }

def IndexedGrammar.Aho.BlockLayout.Boundary.start {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (blocks : List (List g.flag)) : Boundary blocks 0

The initial concrete position is always a block boundary.

Equations

• IndexedGrammar.Aho.BlockLayout.Boundary.start blocks = { blockCount := 0, blockCount_le := ⋯, flagCount_eq := ⋯ }

def IndexedGrammar.Aho.BlockLayout.Boundary.finish {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (blocks : List (List g.flag)) : Boundary blocks blocks.flatten.length

The end of the concrete visible prefix is a block boundary.

Equations

• IndexedGrammar.Aho.BlockLayout.Boundary.finish blocks = { blockCount := blocks.length, blockCount_le := ⋯, flagCount_eq := ⋯ }

def IndexedGrammar.Aho.BlockLayout.Boundary.cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (block : List g.flag) {blocks : List (List g.flag)} {d : ℕ} (boundary : Boundary blocks d) : Boundary (block :: blocks) (block.length + d)

Prefixing one concrete block shifts every old boundary by that block's length.

Equations

• IndexedGrammar.Aho.BlockLayout.Boundary.cons block boundary = { blockCount := boundary.blockCount + 1, blockCount_le := ⋯, flagCount_eq := ⋯ }

def IndexedGrammar.Aho.BlockLayout.Boundary.tail_of_cons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {block : List g.flag} {blocks : List (List g.flag)} {d : ℕ} (hblock : block ≠ []) (boundary : Boundary (block :: blocks) (block.length + d)) : Boundary blocks d

Removing a nonempty first block transports a shifted boundary to the tail partition.

Equations

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

theorem IndexedGrammar.Aho.BlockLayout.Boundary.first_length_le_of_pos {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {block : List g.flag} {blocks : List (List g.flag)} {d : ℕ} (_hblock : block ≠ []) (boundary : Boundary (block :: blocks) d) (hd : 0 < d) : block.length ≤ d

Every positive boundary of a partition beginning with a nonempty block lies at or below the end of that first block. This is the arithmetic fact used to show that a first block is event-free once depth zero is not productive.

def IndexedGrammar.Aho.BlockLayout.Boundary.singletonCons {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (f : g.flag) {blocks : List (List g.flag)} {d : ℕ} (boundary : Boundary blocks d) : Boundary ([f] :: blocks) (d + 1)

A fresh singleton top block shifts every old boundary by exactly one flag.

Equations

• IndexedGrammar.Aho.BlockLayout.Boundary.singletonCons f boundary = ⋯.mp (IndexedGrammar.Aho.BlockLayout.Boundary.cons [f] boundary)

def IndexedGrammar.Aho.BlockLayout.Boundary.extendHead_of_pos {T : Type} {g : IndexedGrammar T} [Fintype g.nt] (f : g.flag) {block : List g.flag} {blocks : List (List g.flag)} {d : ℕ} (hd : 0 < d) (boundary : Boundary (block :: blocks) d) : Boundary ((f :: block) :: blocks) (d + 1)

Extending the first block by one flag shifts every positive boundary by one while keeping the same physical block count.

Equations

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

theorem IndexedGrammar.Aho.BlockLayout.splitAtBoundary {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} {flagCount : ℕ} (layout : BlockLayout g flags blocks word used) (boundary : Boundary blocks flagCount) : ∃ (middle : List (WorkSym g)), BlockLayout g (List.take flagCount flags) (List.take boundary.blockCount blocks) word middle ∧ BlockLayout g flags blocks middle used

Split at an explicitly aligned concrete flag position. The boundary witness makes it impossible for callers to request a split inside the denotation of a compressed block.

theorem IndexedGrammar.Aho.BlockLayout.exists_selectedPrefixes {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) : ∃ (selected : List (WorkSym g)) (selectedUsed : List (WorkSym g)) (tail : List (WorkSym g)), word = selected ++ tail ∧ used = selectedUsed ++ tail ∧ List.countP WorkSym.isIndex selected = blocks.length ∧ List.countP WorkSym.isIndex selectedUsed = blocks.length

The selected physical part of a block layout consists of parallel prefixes followed by one common unselected tail.

theorem IndexedGrammar.Aho.BlockLayout.exists_selectedPrefix_indexCount_eq_blockCount {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {flags : List g.flag} {blocks : List (List g.flag)} {word used : List (WorkSym g)} (layout : BlockLayout g flags blocks word used) : ∃ (selected : List (WorkSym g)) (tail : List (WorkSym g)), word = selected ++ tail ∧ List.countP WorkSym.isIndex selected = blocks.length

Consequently the physical selected-index count is exactly the number of concrete blocks.

Canonical stack-depth event cuts

theorem IndexedGrammar.NFParse.eventDepths_nonempty {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventDepths.Nonempty

Every parse has at least the cut contributed by one terminal leaf.

theorem IndexedGrammar.NFParse.consumesAt_iff_exists_mem_eventDepths_lt {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (k : ℕ) : p.ConsumesAt k ↔ ∃ d ∈ p.eventDepths, k < d

Root-stack position k is consumed exactly when some canonical event cut lies strictly below it. Hence eventDepths is a finite cut profile for every consumption decision made by the bounded scheduler.

theorem IndexedGrammar.NFParse.eventDepths_le_stack_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) : d ∈ p.eventDepths → d ≤ stack.length

Every canonical event depth denotes an actual cut of the current root stack.

theorem IndexedGrammar.NFParse.eventDepths_card_le_productiveCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventDepths.card ≤ p.productiveCount

The finite cut profile uses no more entries than all productive parse events.

theorem IndexedGrammar.NFParse.eventDepths_card_le_twice_yield_length_sub_one {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventDepths.card ≤ 2 * w.length - 1

There are at most 2|w|-1 distinct event cuts. This is the global bound needed when the scheduler allocates at most one compressed index token per canonical cut.

theorem IndexedGrammar.NFParse.productiveCount_eq_twice_yield_length_sub_one {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.productiveCount = 2 * w.length - 1

Productive nodes are exactly the binary nodes plus terminal leaves, hence 2|w|-1.

Coherent productive-event owners

def IndexedGrammar.NFParse.pushEventPreimage (events : Finset ℕ) (d : ℕ) : ℕ

Canonical inverse used when a push maps event depths through Nat.pred. At depth zero we prefer the old zero event when it exists; otherwise the unique relevant preimage is one.

Equations

• IndexedGrammar.NFParse.pushEventPreimage events d = if d = 0 ∧ 0 ∈ events then 0 else d + 1

theorem IndexedGrammar.NFParse.pushEventPreimage_mem {events : Finset ℕ} {d : ℕ} (hd : d ∈ Finset.image Nat.pred events) : pushEventPreimage events d ∈ events

@[simp]

theorem IndexedGrammar.NFParse.pred_pushEventPreimage {events : Finset ℕ} {d : ℕ} (hd : d ∈ Finset.image Nat.pred events) : (pushEventPreimage events d).pred = d

theorem IndexedGrammar.NFParse.pushEventPreimage_injective_on {events : Finset ℕ} {d e : ℕ} (hd : d ∈ Finset.image Nat.pred events) (he : e ∈ Finset.image Nat.pred events) (h : pushEventPreimage events d = pushEventPreimage events e) : d = e

The canonical push inverse is injective on actual image depths.

def IndexedGrammar.NFParse.eventOwnerNat {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) : ℕ

The natural-number code underlying a coherent productive-node ID. Binary roots own zero; left and right child codes occupy disjoint successive ranges. Unary nodes transport codes.

Equations

• One or more equations did not get rendered due to their size.
• (IndexedGrammar.NFParse.terminal hr hlhs hc hrhs).eventOwnerNat d = 0
• (IndexedGrammar.NFParse.pop hr hlhs hc hrhs rest).eventOwnerNat d = rest.eventOwnerNat (d - 1)
• (IndexedGrammar.NFParse.push hr hlhs hc hrhs rest).eventOwnerNat d = rest.eventOwnerNat (IndexedGrammar.NFParse.pushEventPreimage rest.eventDepths d)

theorem IndexedGrammar.NFParse.eventOwnerNat_lt_productiveCount {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {d : ℕ} (hd : d ∈ p.eventDepths) : p.eventOwnerNat d < p.productiveCount

Every actual event code fits inside the productive-node count.

def IndexedGrammar.NFParse.eventOwner {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) (hd : d ∈ p.eventDepths) : Fin p.productiveCount

A coherent productive-node ID for a canonical event depth.

Equations

• p.eventOwner d hd = ⟨p.eventOwnerNat d, ⋯⟩

@[simp]

theorem IndexedGrammar.NFParse.eventOwner_val {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) (hd : d ∈ p.eventDepths) : ↑(p.eventOwner d hd) = p.eventOwnerNat d

theorem IndexedGrammar.NFParse.eventOwnerNat_injective {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {d e : ℕ} (_hd : d ∈ p.eventDepths) (_he : e ∈ p.eventDepths) : p.eventOwnerNat d = p.eventOwnerNat e → d = e

The natural-number event codes are injective on actual event depths.

theorem IndexedGrammar.NFParse.eventOwner_injective {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {d e : ℕ} (hd : d ∈ p.eventDepths) (he : e ∈ p.eventDepths) : p.eventOwner d hd = p.eventOwner e he → d = e

Coherent finite event IDs are injective in the represented stack depth.

@[simp]

theorem IndexedGrammar.NFParse.eventOwnerNat_pop_succ {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = some f) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none]) (rest : g.NFParse B stack w) (d : ℕ) : (pop hr hlhs hc hrhs rest).eventOwnerNat (d + 1) = rest.eventOwnerNat d

@[simp]

theorem IndexedGrammar.NFParse.eventOwnerNat_push {T : Type} {g : IndexedGrammar T} {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (d : ℕ) : (push hr hlhs hc hrhs rest).eventOwnerNat d = rest.eventOwnerNat (pushEventPreimage rest.eventDepths d)

@[simp]

theorem IndexedGrammar.NFParse.eventOwnerNat_binary_zero {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {stack : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (left : g.NFParse B stack u) (right : g.NFParse C stack v) : (binary hr hlhs hc hrhs left right).eventOwnerNat 0 = 0

theorem IndexedGrammar.NFParse.eventOwnerNat_binary_left {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {stack : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (left : g.NFParse B stack u) (right : g.NFParse C stack v) {d : ℕ} (hd0 : d ≠ 0) (hd : d ∈ left.eventDepths) : (binary hr hlhs hc hrhs left right).eventOwnerNat d = left.eventOwnerNat d + 1

theorem IndexedGrammar.NFParse.eventOwnerNat_binary_right {T : Type} {g : IndexedGrammar T} {A B C : g.nt} {stack : List g.flag} {u v : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B none, IRhsSymbol.nonterminal C none]) (left : g.NFParse B stack u) (right : g.NFParse C stack v) {d : ℕ} (hd0 : d ≠ 0) (hd : d ∉ left.eventDepths) : (binary hr hlhs hc hrhs left right).eventOwnerNat d = left.productiveCount + right.eventOwnerNat d + 1

Canonical physical blocks at productive-event cuts

def IndexedGrammar.NFParse.successiveWidths (previous : ℕ) : List ℕ → List ℕ

Successive widths represented by an increasing list of absolute cut positions.

Equations

• IndexedGrammar.NFParse.successiveWidths previous [] = []
• IndexedGrammar.NFParse.successiveWidths previous (d :: ds) = (d - previous) :: IndexedGrammar.NFParse.successiveWidths d ds

@[simp]

theorem IndexedGrammar.NFParse.successiveWidths_length (previous : ℕ) (cuts : List ℕ) : (successiveWidths previous cuts).length = cuts.length

theorem IndexedGrammar.NFParse.successiveWidths_take (previous : ℕ) (cuts : List ℕ) (n : ℕ) : List.take n (successiveWidths previous cuts) = successiveWidths previous (List.take n cuts)

Taking the first n widths is the same as first taking the corresponding cuts.

theorem IndexedGrammar.NFParse.successiveWidths_sum_take_add_previous_eq_getElem {previous : ℕ} {cuts : List ℕ} (hsorted : List.Pairwise (fun (a b : ℕ) => a < b) (previous :: cuts)) (i : ℕ) (hi : i < cuts.length) : (List.take (i + 1) (successiveWidths previous cuts)).sum + previous = cuts[i]

The widths through cut i telescope back to that absolute cut.

theorem IndexedGrammar.NFParse.successiveWidths_pos {previous : ℕ} {cuts : List ℕ} (hsorted : List.Pairwise (fun (a b : ℕ) => a < b) (previous :: cuts)) (width : ℕ) : width ∈ successiveWidths previous cuts → 0 < width

Every width between consecutive strictly increasing cuts is positive.

theorem IndexedGrammar.NFParse.successiveWidths_sum_add_previous_le {previous limit : ℕ} {cuts : List ℕ} (hprevious : previous ≤ limit) (hsorted : List.Pairwise (fun (a b : ℕ) => a < b) (previous :: cuts)) (hcuts : ∀ d ∈ cuts, d ≤ limit) : (successiveWidths previous cuts).sum + previous ≤ limit

Telescoping widths stay inside any common upper bound for the absolute cuts.

def IndexedGrammar.NFParse.eventCuts {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List ℕ

Positive productive-event depths, in their unique increasing order.

Equations

• p.eventCuts = (p.eventDepths.erase 0).sort fun (a b : ℕ) => a ≤ b

@[simp]

theorem IndexedGrammar.NFParse.eventCuts_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventCuts.length = (p.eventDepths.erase 0).card

theorem IndexedGrammar.NFParse.mem_eventCuts_iff {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) : d ∈ p.eventCuts ↔ d ∈ p.eventDepths ∧ d ≠ 0

theorem IndexedGrammar.NFParse.eventCuts_sortedLT {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List.Pairwise (fun (a b : ℕ) => a < b) p.eventCuts

Canonical cuts are strictly increasing.

theorem IndexedGrammar.NFParse.zero_cons_eventCuts_sortedLT {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List.Pairwise (fun (a b : ℕ) => a < b) (0 :: p.eventCuts)

Adding the implicit initial boundary preserves strict increase.

theorem IndexedGrammar.NFParse.eventCuts_le_stack_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (d : ℕ) : d ∈ p.eventCuts → d ≤ stack.length

Every cut is an actual position in the root stack.

theorem IndexedGrammar.NFParse.eventCuts_getLast_le_stack_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (hne : p.eventCuts ≠ []) : p.eventCuts.getLast hne ≤ stack.length

In particular, the last canonical cut lies inside the root stack.

def IndexedGrammar.NFParse.eventWidths {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List ℕ

Concrete lengths of the successive canonical event blocks.

Equations

• p.eventWidths = IndexedGrammar.NFParse.successiveWidths 0 p.eventCuts

@[simp]

theorem IndexedGrammar.NFParse.eventWidths_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventWidths.length = p.eventCuts.length

theorem IndexedGrammar.NFParse.eventWidths_pos {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (width : ℕ) : width ∈ p.eventWidths → 0 < width

theorem IndexedGrammar.NFParse.eventWidths_sum_le_stack_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventWidths.sum ≤ stack.length

The total visible prefix selected by all event cuts fits in the root stack.

theorem IndexedGrammar.NFParse.flatten_splitLengths_eq_take {X : Type} (xs : List X) (widths : List ℕ) (hfit : widths.sum ≤ xs.length) : (widths.splitLengths xs).flatten = List.take widths.sum xs

Splitting a list by widths whose total fits returns exactly the corresponding prefix.

def IndexedGrammar.NFParse.eventBlocks {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List (List g.flag)

Canonical nonempty concrete flag blocks cut from the consumed root-stack prefix.

Equations

• p.eventBlocks = p.eventWidths.splitLengths stack

@[simp]

theorem IndexedGrammar.NFParse.eventBlocks_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventBlocks.length = p.eventCuts.length

theorem IndexedGrammar.NFParse.eventBlocks_map_length {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : List.map List.length p.eventBlocks = p.eventWidths

Each physical block has exactly its positive successive width.

theorem IndexedGrammar.NFParse.eventBlocks_nonempty {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (block : List g.flag) : block ∈ p.eventBlocks → block ≠ []

No canonical physical block is empty.

theorem IndexedGrammar.NFParse.eventBlocks_flatten {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventBlocks.flatten = List.take p.eventWidths.sum stack

The generated blocks flatten to the concrete stack prefix ending at the final event cut.

theorem IndexedGrammar.NFParse.eventWidths_sum_take_eq_getElem {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : ℕ) (hi : i < p.eventCuts.length) : (List.take (i + 1) p.eventWidths).sum = p.eventCuts[i]

Widths through the ith block telescope to the ith absolute event cut.

theorem IndexedGrammar.NFParse.eventBlocks_take_flatten_eq_take_getElem {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : ℕ) (hi : i < p.eventCuts.length) : (List.take (i + 1) p.eventBlocks).flatten = List.take p.eventCuts[i] stack

Every prefix of canonical blocks ends at the corresponding absolute event cut.

theorem IndexedGrammar.NFParse.eventBlocks_take_flatten_length_eq_getElem {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : ℕ) (hi : i < p.eventCuts.length) : (List.take (i + 1) p.eventBlocks).flatten.length = p.eventCuts[i]

Numerically, the prefix endpoints of eventBlocks are exactly eventCuts.

theorem IndexedGrammar.NFParse.eventCuts_nodup {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventCuts.Nodup

The canonical cut list has no duplicate endpoints.

def IndexedGrammar.NFParse.eventBlockOwner {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : Fin p.eventBlocks.length) : ℕ

Assign a physical block its productive-event-depth owner: the endpoint of that block.

Equations

• p.eventBlockOwner i = (List.take (↑i + 1) p.eventBlocks).flatten.length

theorem IndexedGrammar.NFParse.eventBlockOwner_mem_eventDepths {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : Fin p.eventBlocks.length) : p.eventBlockOwner i ∈ p.eventDepths

Every physical block owner is an actual productive-event depth.

theorem IndexedGrammar.NFParse.eventBlockOwner_injective {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : Function.Injective p.eventBlockOwner

Different physical blocks receive different productive-event-depth owners. This is the global injection needed for the token budget; unlike one-way boundary compatibility it rules out arbitrary extra protected-child blocks.

def IndexedGrammar.NFParse.eventBlockGlobalOwner {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : Fin p.eventBlocks.length) : Fin (2 * w.length - 1)

Root-capacity owner of a canonical physical block. Unlike its raw depth endpoint, this ID is stable under the unary transports and binary embeddings encoded by eventOwnerNat.

Equations

• p.eventBlockGlobalOwner i = Fin.cast ⋯ (p.eventOwner (p.eventBlockOwner i) ⋯)

@[simp]

theorem IndexedGrammar.NFParse.eventBlockGlobalOwner_val {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) (i : Fin p.eventBlocks.length) : ↑(p.eventBlockGlobalOwner i) = p.eventOwnerNat (p.eventBlockOwner i)

theorem IndexedGrammar.NFParse.eventBlockGlobalOwner_injective {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : Function.Injective p.eventBlockGlobalOwner

Canonical block owners are globally collision-free in the exact 2|w|-1 carrier.

theorem IndexedGrammar.NFParse.exists_eventBlocks_boundary {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) {d : ℕ} (hd : d ∈ p.eventDepths) : ∃ blockCount ≤ p.eventBlocks.length, d = (List.take blockCount p.eventBlocks).flatten.length

Every productive-event depth is a whole-block prefix boundary (with depth zero represented by the empty block prefix).

theorem IndexedGrammar.NFParse.eventBlocks_length_le_twice_yield_length_sub_one {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventBlocks.length ≤ 2 * w.length - 1

The number of canonical physical blocks obeys the same 2|w|-1 bound as event cuts.

def IndexedGrammar.NFParse.eventBlocksOwnership {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : Aho.BlockOwnership (2 * w.length - 1) p.eventBlocks

Canonical blocks come with a persistent finite ownership carrier of the exact global 2|w|-1 capacity. Descendants can retain these owners through take/drop, so protected boundaries remain charged even when they are extra relative to the child's local event cuts.

Equations

• p.eventBlocksOwnership = { owners := List.ofFn p.eventBlockGlobalOwner, owners_length := ⋯, owners_nodup := ⋯ }

@[simp]

theorem IndexedGrammar.NFParse.eventBlocksOwnership_owners {T : Type} {g : IndexedGrammar T} {A : g.nt} {stack : List g.flag} {w : List T} (p : g.NFParse A stack w) : p.eventBlocksOwnership.owners = List.ofFn p.eventBlockGlobalOwner