ColumnCodeUniverse.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite universe for every column with the proved numerical budget.

def OAI.TwoPointCorrelations.columnBudgetCap line 12
abbrev OAI.TwoPointCorrelations.BudgetColumnCode line 15
def OAI.TwoPointCorrelations.decodeBudgetColumnPattern line 18
theorem OAI.TwoPointCorrelations.budget_column_code_of_counts line 24
Source documentation
The cap depends only on the common scale and forest size, not on the numerical coefficients, the prime values, or the number of regular lines.
```
theorem budget_column_code_of_counts {n N S O I : ℕ} {L : ℝ}
    (hn : n ≤ N) (hS : S ≤ N) (hO : O ≤ N) (hI : I ≤ N)
    (hcost : ((2 * S + O + I : ℕ) : ℝ) ≤ 66 * L ^ (0.92 : ℝ))
    (code : ColumnDecoderCode N S O I) :
    ∃ full : BudgetColumnCode N L,
      decodeBudgetColumnPattern hn full = decodeColumnPrefixPattern hn code := by
…
```
Mentions: OAI.TwoPointCorrelations.ColumnDecoderCode, OAI.TwoPointCorrelations.BudgetColumnCode, OAI.TwoPointCorrelations.decodeBudgetColumnPattern, OAI.TwoPointCorrelations.decodeColumnPrefixPattern
theorem OAI.TwoPointCorrelations.eventually_budget_column_code_card line 45
Source documentation
All permitted counts are included simultaneously. The factor 264 is absorbed only into the large-scale threshold; the exponential constant 64 is the same for every column and every choice of numerical coefficients.
```
theorem eventually_budget_column_code_card :
    ∀ᶠ L : ℝ in atTop, ∀ k N : ℕ,
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 1 ≤ N → N ≤ 4 * k →
      (Fintype.card (BudgetColumnCode N L) : ℝ) ≤ Real.exp (64 * k) := by
…
```
Mentions: OAI.TwoPointCorrelations.BudgetColumnCode
theorem OAI.TwoPointCorrelations.card_budget_column_patterns line 62
abbrev OAI.TwoPointCorrelations.BudgetColumnArrayCode line 72
instance OAI.TwoPointCorrelations.budgetColumnArrayFintype line 75
def OAI.TwoPointCorrelations.decodeBudgetColumnArray line 81
theorem OAI.TwoPointCorrelations.budget_column_array_cover line 85
theorem OAI.TwoPointCorrelations.eventually_budget_column_array_card line 95
Source documentation
The full column pattern array has cost exponential in J*k, with one universal finite set for all numerical assignments.
```
theorem eventually_budget_column_array_card :
    ∀ᶠ L : ℝ in atTop, ∀ k J N : ℕ,
      L / 2 ≤ (k : ℝ) → (k : ℝ) ≤ L → 1 ≤ N → N ≤ 4 * k →
      (Fintype.card (BudgetColumnArrayCode J N L) : ℝ) ≤ Real.exp (64 * k * J) := by
…
```
Mentions: OAI.TwoPointCorrelations.BudgetColumnArrayCode