RegularColumnNames.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Name regular perfect classes by forest vertices and omitted classes by occurrences.

def OAI.TwoPointCorrelations.forestPerfectName line 13
Source documentation
Omitted classes use bounded occurrence indices. Regular classes use exactly the line-vertex numbers shared across the path family.
```
def forestPerfectName (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ) (i : Fin n) : ℕ ⊕ ℕ :=
…
```
theorem OAI.TwoPointCorrelations.forestPerfectName_of_label_eq line 18

theorem OAI.TwoPointCorrelations.forestPerfectName_eq_iff line 31

Source documentation

Injectivity is needed only for lines observed at perfect positions. No numbering requirement is imposed on unused regular labels.

theorem forestPerfectName_eq_iff (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ)
    (hinj : ∀ i ∈ perfect, ∀ j ∈ perfect, ∀ (hi : label i ∈ regular) (hj : label j ∈ regular),
      number ⟨label i, hi⟩ = number ⟨label j, hj⟩ → label i = label j)
    (i : Fin n) (hi : i ∈ perfect) (j : Fin n) (hj : j ∈ perfect) :
    forestPerfectName label perfect regular number i = forestPerfectName label perfect regular number j ↔
      label i = label j := by
…

Mentions: OAI.TwoPointCorrelations.forestPerfectName

theorem OAI.TwoPointCorrelations.canonical_forest_name_eq_iff line 51

Source documentation

The completed names represent the full equality pattern, including classes having no perfect occurrence.

theorem canonical_forest_name_eq_iff (label : Fin n → α) (perfect : Finset (Fin n))
    (regular : Finset α) (number : regular → ℕ)
    (hinj : ∀ i ∈ perfect, ∀ j ∈ perfect, ∀ (hi : label i ∈ regular) (hj : label j ∈ regular),
      number ⟨label i, hi⟩ = number ⟨label j, hj⟩ → label i = label j)
    (i j : Fin n) :
    canonicalColumnName label perfect (forestPerfectName label perfect regular number) i =
      canonicalColumnName label perfect (forestPerfectName label perfect regular number) j ↔ label i = label j := by
…

Mentions: OAI.TwoPointCorrelations.canonicalColumnName, OAI.TwoPointCorrelations.forestPerfectName