OAI/Combinatorics/ContingencyTables/Counting/CompanionCanonicalPhaseSupport.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Representation preservation for every executed counting phase

The restart support statement is obtained from its actual finite-word law. The remaining trajectory and observation words may be unused padding for that law; their presence still supplies the required precision markers.

  1. lemma OAI.ContingencyTables.CompanionCanonicalPhaseSupport.restart_prefix_le line 21
  2. theorem OAI.ContingencyTables.CompanionCanonicalPhaseSupport.output_rep line 39