OAI/NumberTheory/TwoPoint/Walks/WeightedWordCircuit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact signed state expansion for a closed word. The padding states are truncated; every centered-prime bit is retained. The remaining predicate is a circuit, including all prohibited-vertex tests.

  1. def OAI.TwoPointCorrelations.weightedStateCircuit line 15
  2. lemma OAI.TwoPointCorrelations.weightedStateCircuit_eval line 22
  3. lemma OAI.TwoPointCorrelations.weightedStateCircuit_depth line 34
  4. lemma OAI.TwoPointCorrelations.weightedStateCircuit_size line 46
  5. theorem OAI.TwoPointCorrelations.weightedWord_scalar_expansion line 55
  6. lemma OAI.TwoPointCorrelations.weightedWord_coefficient_mass line 101