QuotientRunPaths.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Constant perfect runs give the concrete reduced paths used by column coding.

def OAI.TwoPointCorrelations.QuotientRunData line 16

Source documentation

Each transition ends a nonzero constant run and starts the next regular label on its common quotient line. These are local conditions on departures.

def QuotientRunData (D : Submodule K (α → K))
    (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
    (label : ℕ → α) (coefficient : ℕ → K) (a : ℕ) (i : ι) :
    List (ℕ × ι) → Prop
  | [] => True
  | (b, j) :: rest =>
      a ≤ b ∧ (∀ t ∈ Ico a b, label t = regularLabel i) ∧
      (∑ t ∈ Ico a b, coefficient t) ≠ 0 ∧ i ≠ j ∧
      (∃ c : K, D.mkQ (formalDeparture label coefficient b) = anchor j +
        c • D.mkQ (Pi.basisFun K α (regularLabel j))) ∧
      QuotientRunData D anchor regularLabel label coefficient b j rest

Mentions: OAI.TwoPointCorrelations.formalDeparture

def OAI.TwoPointCorrelations.quotientRunSteps line 28

theorem OAI.TwoPointCorrelations.quotientRunData_incidenceChain line 33

Source documentation

Both adjacent lines contain the exact common departure at a transition.

theorem quotientRunData_incidenceChain (D : Submodule K (α → K))
    (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
    (label : ℕ → α) (coefficient : ℕ → K) (a : ℕ) (i : ι) (steps : List (ℕ × ι))
    (hstart : ∃ c : K, D.mkQ (formalDeparture label coefficient a) = anchor i +
      c • D.mkQ (Pi.basisFun K α (regularLabel i)))
    (hdata : QuotientRunData D anchor regularLabel label coefficient a i steps) :
    IncidenceChain (K := K) anchor (fun j => D.mkQ (Pi.basisFun K α (regularLabel j))) i
…

Mentions: OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.QuotientRunData, OAI.TwoPointCorrelations.IncidenceChain

theorem OAI.TwoPointCorrelations.quotientRunData_reduced line 52

Source documentation

Nonzero numerical runs prohibit point--line--point reversal; distinct adjacent run labels prohibit line--point--line reversal.

theorem quotientRunData_reduced (D : Submodule K (α → K))
    (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
    (label : ℕ → α) (coefficient : ℕ → K)
    (hdir : ∀ j, D.mkQ (Pi.basisFun K α (regularLabel j)) ≠ 0)
    (a : ℕ) (i : ι) (steps : List (ℕ × ι))
    (hdata : QuotientRunData D anchor regularLabel label coefficient a i steps) :
    IncidenceReduced i (quotientRunSteps D label coefficient steps) := by
…

Mentions: OAI.TwoPointCorrelations.QuotientRunData, OAI.TwoPointCorrelations.IncidenceReduced, OAI.TwoPointCorrelations.quotientRunSteps

theorem OAI.TwoPointCorrelations.quotientRunData_simple line 79

Source documentation

The path support consists of exactly the canonical regular run lines alternating with their actual transition departures.

theorem quotientRunData_simple (D : Submodule K (α → K))
    (anchor : ι → (α → K) ⧸ D) (regularLabel : ι → α)
    (label : ℕ → α) (coefficient : ℕ → K)
    (hind : LinearIndependent K (fun j => D.mkQ (Pi.basisFun K α (regularLabel j))))
    (a : ℕ) (i : ι) (steps : List (ℕ × ι))
    (hstart : ∃ c : K, D.mkQ (formalDeparture label coefficient a) = anchor i +
      c • D.mkQ (Pi.basisFun K α (regularLabel i)))
    (hdata : QuotientRunData D anchor regularLabel label coefficient a i steps) :
    (Walk.ofSupport (incidenceVertices i (quotientRunSteps D label coefficient steps))
      (incidenceVertices_ne_nil _ _)
      (incidenceVertices_isChain anchor _ _ _
        (quotientRunData_incidenceChain D anchor regularLabel label coefficient a i steps hstart hdata))).IsPath := by
…

Mentions: OAI.TwoPointCorrelations.formalDeparture, OAI.TwoPointCorrelations.QuotientRunData, OAI.TwoPointCorrelations.incidenceVertices, OAI.TwoPointCorrelations.quotientRunSteps, OAI.TwoPointCorrelations.incidenceVertices_ne_nil, OAI.TwoPointCorrelations.incidenceVertices_isChain, OAI.TwoPointCorrelations.quotientRunData_incidenceChain