OAI/Combinatorics/ContingencyTables/Counting/CompanionRestartSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Every executed restart has the canonical paired catalog

Finite uniform words have positive mass individually. The proved padded restart law therefore gives a valid encoded source state on every word, including words on which one of the return attempts uses its fallback.

  1. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.catalog_length_encode line 22
  2. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.catalog_length_of_supported line 28
  3. lemma OAI.ContingencyTables.CompanionInitializedRestartProgram.outer_trial_catalog line 36
  4. theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.outer_output_rep_of_supported line 40
  5. theorem OAI.ContingencyTables.CompanionInitializedRestartProgram.output_padded_supported line 55