OAI/Combinatorics/TreeEdit/TorusLowerBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TreeEdit.singletonCode line 10
2. lemma OAI.TreeEdit.encode_singletonCode line 12
3. theorem OAI.TreeEdit.TorusTree.binary_witness line 21
4. lemma OAI.TreeEdit.TorusTree.witnesses_eventually line 97
5. theorem OAI.TreeEdit.binary_torus line 106

   Distinct definitions of this name: ComparatorChallenges/TreeEdit.lean:46 (same statement text; different proof or body). Qualify references as OAI.TreeEdit.binary_torus@path.