OAI/NumberTheory/TwoPoint/Bounds/ActiveStateVectors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous bounded active states at every vertex of a trace word. Offsets may share residue coordinates; the circuit keeps this sharing explicit.

  1. def OAI.TwoPointCorrelations.activeStateVectorCircuit line 13
  2. lemma OAI.TwoPointCorrelations.activeStateVectorCircuit_eval line 17
  3. lemma OAI.TwoPointCorrelations.activeStateVectorCircuit_depth line 24
  4. lemma OAI.TwoPointCorrelations.activeStateVectorCircuit_size line 31
  5. theorem OAI.TwoPointCorrelations.activeStateVector_scalar_expansion line 36
  6. lemma OAI.TwoPointCorrelations.activeStateVector_coefficient_mass line 74
  7. lemma OAI.TwoPointCorrelations.activeStateVector_size_budget line 87
  8. lemma OAI.TwoPointCorrelations.activeStateVector_coefficient_budget line 108