ColumnGeometryEncoding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

From quotient-line geometry to a complete column code, including the empty regular set.

theorem OAI.TwoPointCorrelations.partition_all_omitted line 11
theorem OAI.TwoPointCorrelations.indexedRegularSegments_eq_nil line 17
def OAI.TwoPointCorrelations.emptyForestPathCode line 31

theorem OAI.TwoPointCorrelations.column_code_from_quotient_geometry line 38

Source documentation

The only geometric premises are independent quotient directions, actual line incidence, and nonzero constant intervals. All path codes, canonical labels, occurrence references and the full equality pattern are constructed. No nonemptiness of the regular set is required.

theorem column_code_from_quotient_geometry {α : Type*} [Fintype α] [DecidableEq α]
    {n N O I : ℕ} (hN : 0 < N) (hn : n ≤ N)
    (label : Fin n → α) (perfect : Finset (Fin n)) (regular : Finset α)
    (labelNat : ℕ → α) (coefficient : ℕ → ℝ)
    (chunks : List (List α ⊕ α)) (blocks : List (ℕ × ℕ))
    (hentries : columnChunkEntries chunks =
      (columnPositionEntries perfect).map (fun p => (label p.1, p.2)))
    (hblocks : chunks.filterMap (Sum.elim some (fun _ => none)) =
      blocks.map (fun b => blockLabelList labelNat b.1 b.2))
    (D : Submodule ℝ (α → ℝ)) (anchor : regular → (α → ℝ) ⧸ D)
    (hind : LinearIndependent ℝ (fun z : regular => D.mkQ (Pi.basisFun ℝ α z)))
    (hline : ∀ b ∈ blocks, ∀ t ∈ Ico b.1 (b.1 + b.2), ∀ ht : labelNat t ∈ regular,
…

Mentions: OAI.TwoPointCorrelations.columnChunkEntries, OAI.TwoPointCorrelations.columnPositionEntries, OAI.TwoPointCorrelations.blockLabelList