OAI/NumberTheory/TwoPoint/Circuits/CircuitTreeWalk.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A longest branch of the concrete canonical tree supplies a query walk with at least that many queried variables.

  1. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.queryVariables_depth_state line 16
  2. lemma OAI.TwoPointCorrelations.BooleanDecisionTree.queryVariables_depth_witness line 49
  3. lemma OAI.TwoPointCorrelations.CubeTerm.satisfied_of_live_empty line 65
  4. theorem OAI.TwoPointCorrelations.canonicalDNFTree_depth_walk line 75