PreprocessingRegularLoopWords.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Prefix and suffix invariants for regular-table row loops

These finite block identities apply to original-vertex blocks, to dummy blocks within an owner, and to whole owner blocks. They expose exactly the next emitted block while preserving the codec's established order.

def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix line 17
Source documentation
Bits emitted by the first k blocks.
```
def blocksPrefix {n : Nat} (f : Fin n → List Bool) (k : Nat) : List Bool :=
…
```
def OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix line 21
Source documentation
Bits remaining after the first k blocks.
```
def blocksSuffix {n : Nat} (f : Fin n → List Bool) (k : Nat) : List Bool :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_zero line 24
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_all line 28
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_succ line 34
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_zero line 42
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_all line 46
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_succ line 52
theorem OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_append_suffix line 60
Source documentation
The completed and remaining portions partition the original bitstream.
```
theorem blocksPrefix_append_suffix {n : Nat} (f : Fin n → List Bool) (k : Nat) :
    blocksPrefix f k ++ blocksSuffix f k = (List.ofFn f).flatten := by
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix, OAI.MaxCutGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix