ColumnCode.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Counting the finite column-code universe

The shape is a typed plane forest on at most N vertices. Binary marks record boundaries and run types. Omitted runs and imperfect positions store representative indices; regular segments store their two endpoints.

instance OAI.TwoPointCorrelations.boundedForestFinite line 15
instance OAI.TwoPointCorrelations.boundedForestFintype line 18
abbrev OAI.TwoPointCorrelations.ColumnCode line 22
Source documentation
Fixed-size slots can be padded once the nonempty index universe is fixed.
```
abbrev ColumnCode (N segments omitted imperfect : ℕ) :=
…
```

theorem OAI.TwoPointCorrelations.card_columnCode_le line 28

Source documentation

The code count is uniform over every numerical realization.

theorem card_columnCode_le (N segments omitted imperfect : ℕ) :
    Fintype.card (ColumnCode N segments omitted imperfect) ≤
      2 ^ (5 * N + 1) * N ^ (2 * segments + omitted + imperfect) := by
…

Mentions: OAI.TwoPointCorrelations.ColumnCode

theorem OAI.TwoPointCorrelations.patterns_le_columnCode line 46

Source documentation

A decoder makes different equality patterns use different codes, with no numerical coefficients present in the finite counting universe.

theorem patterns_le_columnCode {Pattern : Type*} [Fintype Pattern]
    (N segments omitted imperfect : ℕ)
    (encode : Pattern → ColumnCode N segments omitted imperfect)
    (decode : ColumnCode N segments omitted imperfect → Pattern)
    (hdecode : ∀ p, decode (encode p) = p) :
    Fintype.card Pattern ≤ 2 ^ (5 * N + 1) * N ^ (2 * segments + omitted + imperfect) := by
…

Mentions: OAI.TwoPointCorrelations.ColumnCode