Per-axis TabAt from ChunkTabBnd6

Open

J6Seg.Ax.tabAt_of

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

j6segkappa-r6tables

The global package ChunkTabBnd6 P is definitionally the eventual per-axis table bound TabAt.

Unpacking the existential yields a threshold $n_1$ such that every admissible axis carries TabAt. This is the bridge from the uniform table lemma to the per-axis hypothesis of chunk_budget_at.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false

open J6Seg J6Seg.Ax
open IntMul.Kappa.R6

Formal statement

namespace J6Seg.Ax

theorem tabAt_of (P : Prm) (h : ChunkTabBnd6 P) :
    ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src →
      ∀ D : ℕ, dP6 P n = D + 1 → ∀ k ≤ D, TabAt P n src k := by
  sorry

end J6Seg.Ax

Source

xuanji round-six (Solutions.J6SegAx facts); definitional bridge ChunkTabBnd6 → TabAt; feeds chunkBudget6_all

View graph