OAI/NumberTheory/TwoPoint/Bounds/PrimeSlotCode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

A complete equality-pattern code for tuple and padding prime occurrences.

  1. structure OAI.TwoPointCorrelations.PrimeSlotData line 15

    Source documentation

    Each occurrence records its step, whether it belongs to the padding, and its numerical prime. Unused slots are avoided by taking the actual total length.

    structure PrimeSlotData (R N : ℕ) where
…
  2. def OAI.TwoPointCorrelations.PrimeSlotData.slots line 25
  3. def OAI.TwoPointCorrelations.PrimeSlotData.factor line 28
  4. def OAI.TwoPointCorrelations.PrimeSlotData.word line 31
  5. def OAI.TwoPointCorrelations.PrimeSlotData.code line 34
  6. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_class_eq_iff line 37
  7. lemma OAI.TwoPointCorrelations.PrimeSlotData.code_class_prime line 41
  8. def OAI.TwoPointCorrelations.CrudeWordCode.usedClasses line 51
  9. def OAI.TwoPointCorrelations.CrudeWordCode.classAt line 53
  10. def OAI.TwoPointCorrelations.CrudeWordCode.primeData line 56
  11. def OAI.TwoPointCorrelations.CrudeWordCode.numericalWord line 62
  12. lemma OAI.TwoPointCorrelations.CrudeWordCode.primeData_encode line 65
  13. lemma OAI.TwoPointCorrelations.CrudeWordCode.numericalWord_encode line 74
  14. lemma OAI.TwoPointCorrelations.CrudeWordCode.numericalWord_length line 78
  15. lemma OAI.TwoPointCorrelations.CrudeWordCode.numericalWord_get line 84

    Source documentation

    Padding is reconstructed from the same prime classes as tuple factors, so repetitions across steps never introduce new independent numerical choices.

    lemma numericalWord_get (c : CrudeWordCode R N R) (value : c.usedClasses → ℕ) (i : Fin R) :
    (c.numericalWord value)[i.val]'(by rw [numericalWord_length]; exact i.isLt) =
      ⟨c.1 i,
        ∏ j ∈ univ.filter (fun j => c.2.2.1 j = i ∧ c.2.2.2 j = false), value (c.classAt j),
        ∏ j ∈ univ.filter (fun j => c.2.2.1 j = i ∧ c.2.2.2 j = true), value (c.classAt j)⟩ := by
…

    Mentions: OAI.TwoPointCorrelations.CrudeWordCode, OAI.TwoPointCorrelations.CrudeWordCode.numericalWord_length