QuotientPathNumbering.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One bounded numbering for the regular lines in all actual quotient paths.

theorem OAI.TwoPointCorrelations.inl_mem_incidenceVertices line 12

theorem OAI.TwoPointCorrelations.quotient_run_family_numbering line 24

Source documentation

The same forest numbering is used for every regular segment. Equal line numbers therefore identify exactly equal regular labels across all blocks.

theorem quotient_run_family_numbering {S N : ℕ}
    (D : Submodule K (α → K)) (anchor : ι → (α → K) ⧸ D)
    (regularLabel : ι → α) (label : ℕ → α) (coefficient : ℕ → K)
    (hind : LinearIndependent K (fun j => D.mkQ (Pi.basisFun K α (regularLabel j))))
    (start : Fin S → ℕ) (first : Fin S → ι) (steps : Fin S → List (ℕ × ι))
    (hstart : ∀ i, ∃ c : K, D.mkQ (formalDeparture label coefficient (start i)) =
      anchor (first i) + c • D.mkQ (Pi.basisFun K α (regularLabel (first i))))
    (hdata : ∀ i, QuotientRunData D anchor regularLabel label coefficient (start i) (first i) (steps i))
    (hsize : (∑ i, (2 * (steps i).length + 1)) ≤ N) :
    ∃ (number : ι → ℕ) (code : ForestPathData.Code N S),
      (∀ i j, j ∈ first i :: (steps i).map Prod.snd → number j < N) ∧
      (∀ i j, j ∈ first i :: (steps i).map Prod.snd →
…

Mentions: OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.QuotientRunData, OAI.TwoPointCorrelations.ForestPathData.Code