IntegerShiftGeometry.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Numerical words attached to the forced paths in the actual trace expansion.

def OAI.TwoPointCorrelations.integerStepWord line 14
lemma OAI.TwoPointCorrelations.integerShiftEnd_site line 18
lemma OAI.TwoPointCorrelations.integer_closed_word_displacement line 30
lemma OAI.TwoPointCorrelations.signedIntegerWeight_flip line 40

lemma OAI.TwoPointCorrelations.signedIntegerWeight_departure line 50

Source documentation

Periodicity permits using the departure center in both orientations. All surviving cutoffs remain literal indicator conditions.

lemma signedIntegerWeight_departure (Q : Finset ℕ) (u : ℕ → ℝ)
    (eligible : ℕ → Prop) (g center : ℤ → ℝ) (L K : ℝ)
    (extra : ℤ → Prop) (h : ℕ) (a : SignedStep) (n : ℤ)
    (hperiod : ∀ q ∈ Q, ∀ z, center (z + (h * q * a.tuple : ℕ)) = center z) :
    signedIntegerWeight Q u eligible g center L K extra h a n =
      if a.padding ∈ Q ∧ eligible a.padding ∧ (a.padding : ℤ) ∣ n ∧
        integerEdgeKeep Q u eligible g L K extra n ∧
        integerEdgeKeep Q u eligible g L K extra (n + a.displacement h) then
        L * u a.padding * center n / (g n * g (n + a.displacement h)) else 0 := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.signedIntegerWeight, OAI.TwoPointCorrelations.integerEdgeKeep

lemma OAI.TwoPointCorrelations.integerShiftWeight_nonzero line 87

theorem OAI.TwoPointCorrelations.integerShiftWord_chain line 103

Source documentation

Every nonzero half of the trace is nonbacktracking in its tuple labels. The two halves can be joined without imposing a new condition at the joins.

theorem integerShiftWord_chain (embed : V → D × ℤ) (Q : Finset ℕ) (tuple : D → ℕ)
    (u : ℕ → ℝ) (eligible : D → ℕ → Prop) (g : ℤ → ℝ) (center : D → ℤ → ℝ)
    (L K : ℝ) (extra : D → ℤ → Prop) (h : ℕ) (gate : D → ℤ → ℤ → Prop)
    {k : ℕ} (x : D × ℤ) (w : Fin k → D × (Q × Bool))
    (hw : shiftWordWeight embed (integerShiftNext Q tuple h)
      (integerShiftWeight Q tuple u eligible g center L K extra h gate) x w ≠ 0) :
    (x.1 :: (List.ofFn w).map Prod.fst).IsChain (fun a b => a ≠ b) := by
…

Mentions: OAI.TwoPointCorrelations.shiftWordWeight, OAI.TwoPointCorrelations.integerShiftNext, OAI.TwoPointCorrelations.integerShiftWeight

lemma OAI.TwoPointCorrelations.integerStateEmbedding_injective line 124

theorem OAI.TwoPointCorrelations.integer_matrix_moment_forced_words line 132

Source documentation

The concrete nonbacktracking integer matrix has the forced-word moment formula, with exactly one freely chosen starting site.

theorem integer_matrix_moment_forced_words
    (site : V → ℤ) (hinj : Function.Injective site) (Q : Finset ℕ) (tuple : D → ℕ)
    (u : ℕ → ℝ) (eligible : D → ℕ → Prop) (g : ℤ → ℝ) (center : D → ℤ → ℝ)
    (L K : ℝ) (extra : D → ℤ → Prop) (h : ℕ) (gate : D → ℤ → ℤ → Prop) (k : ℕ) :
    matrixFrobeniusSq (blockNonbacktrackingMatrix (fun d i j =>
      if gate d (site i) (site j) then
        integerEdgeMatrix site Q u (eligible d) g (center d) L K (extra d) h (tuple d) i j
      else 0) ^ k) =
      ∑ x : D × V, ∑ a : Fin k → D × (Q × Bool), ∑ b : Fin k → D × (Q × Bool),
        if shiftWordEnd (integerShiftNext Q tuple h) (x.1, site x.2) a =
          shiftWordEnd (integerShiftNext Q tuple h) (x.1, site x.2) b then
          shiftWordWeight (fun x : D × V => (x.1, site x.2)) (integerShiftNext Q tuple h)
…

Mentions: OAI.TwoPointCorrelations.matrixFrobeniusSq, OAI.TwoPointCorrelations.blockNonbacktrackingMatrix, OAI.TwoPointCorrelations.integerEdgeMatrix, OAI.TwoPointCorrelations.shiftWordEnd, OAI.TwoPointCorrelations.integerShiftNext, OAI.TwoPointCorrelations.shiftWordWeight