Native enumeration of all query chunks

The controller reads the actual class-count table produced by Classes.program and calls the existing native chunk writer for each class. Descriptors are concatenated without padding; their query pointers refer to the original disjoint class arrays. No descriptor layout or prefix table is supplied by the caller.

This composes the class and chunk loops in the pinned Theorem 17 construction.

Main definitions

• ChunkCatalogue.program: fixed thirty-two-register descriptor controller.
• ChunkCatalogue.before: the mathematical number of descriptors preceding a class.

Main results

• ChunkCatalogue.exec: charged enumeration of the actual class counts, exact descriptor readback and preservation outside the concatenated output.
• ChunkCatalogue.before_index: unique class/chunk coordinates for every occupied output slot, using Mathlib's existing finite sigma enumeration.
• ChunkCatalogue.before_le, ChunkCatalogue.before_add_lt: descriptor allocation bounds.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.counts : Fin 32

Class-count table pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.queries : Fin 32

Base of the class query blocks, each of capacity 2n² words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.size : Fin 32

Matrix side length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.modulus : Fin 32

Number of residue classes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.dst : Fin 32

Beginning of the contiguous output descriptor array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.capacity : Fin 32

Positive maximum pairs per chunk.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.cursor : Fin 32

Current class.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.written : Fin 32

Total number of descriptors written so far.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.heap : Fin 32

First free descriptor address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.one : Fin 32

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.three : Fin 32

Number of words per descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.addr : Fin 32

Current count-table address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.stride : Fin 32

Capacity of one class query block, in words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.temp : Fin 32

Descriptor-length temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkQueries : Fin 32

Query pointer passed to the chunk writer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkDst : Fin 32

Output pointer passed to the chunk writer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkTotal : Fin 32

Loaded class count passed to the chunk writer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkCapacity : Fin 32

Chunk capacity passed to the chunk writer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkResidue : Fin 32

Residue passed to the chunk writer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunkCount : Fin 32

Number of descriptors returned by the chunk writer.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.chunks : WordRAM.Code WordRAM.Basis.standard 32

Call the existing native chunk writer in the lower register bank.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.deliver : WordRAM.Code WordRAM.Basis.standard 32

Read the current count and deliver its actual query pointer to the chunk writer.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.advance : WordRAM.Code WordRAM.Basis.standard 32

Advance the output heap by the number of descriptors actually written.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.body : WordRAM.Code WordRAM.Basis.standard 32

One class, including empty classes.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.program : WordRAM.Code WordRAM.Basis.standard 32

Initialize the concatenation cursor and run every residue class.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.program_fixed : program.size ≤ 80 ∧ ¬program.ReadsWidth

The complete controller is fixed code and does not inspect physical width.

def Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.before (C : ℕ → ℕ) (cap rho : ℕ) : ℕ

Number of actual chunk descriptors for all classes strictly below rho.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.before_add_lt (C : ℕ → ℕ) (cap : ℕ) {rho p k : ℕ} (hrho : rho < p) (hk : k < C rho ⌈/⌉ cap) : before C cap rho + k < before C cap p

Every actual chunk lies strictly within the concatenated descriptor array.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.before_index (C : ℕ → ℕ) (cap p i : ℕ) (hi : i < before C cap p) : ∃! idx : (rho : Fin p) × Fin (C ↑rho ⌈/⌉ cap), i = before C cap ↑idx.fst + ↑idx.snd

Every occupied descriptor slot names exactly one class and one chunk. This is the existing finSigmaFinEquiv, expressed with the same prefix sum as the native concatenation loop.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.before_le {C : ℕ → ℕ} {cap p N : ℕ} (hcap : 0 < cap) (hC : ∀ r < p, C r ≤ N) {rho : ℕ} (hrho : rho ≤ p) : before C cap rho ≤ rho * N

At most N queries per class give at most rho * N occupied descriptors, since every nonempty chunk contains at least one query. This bounds the actual allocation before matrix preparation as well as the descriptor controller's own arithmetic.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ChunkCatalogue.exec {w : ℕ} (x : WordRAM.Data 32) (C : ℕ → ℕ) (hread : ∀ r < x.regs modulus, x.mem (x.regs counts + r) = C r) (hC : ∀ r < x.regs modulus, C r ≤ x.regs size * x.regs size) (hcap : 0 < x.regs capacity) (hcounts : x.regs counts + x.regs modulus ≤ x.regs dst) (hqueries : x.regs queries + 2 * x.regs modulus * (x.regs size * x.regs size) ≤ x.regs dst) (hfit : WordRAM.Fits w (x.regs dst + 5 * x.regs modulus * (x.regs size * x.regs size) + x.regs counts + x.regs modulus + x.regs queries + 2 * (x.regs size * x.regs size) + 5)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w program x y (x.regs modulus * (17 * (x.regs size * x.regs size) + 20) + 9) ∧ y.regs written = before C (x.regs capacity) (x.regs modulus) ∧ y.regs heap = x.regs dst + 3 * y.regs written ∧ (∀ (i : Fin 32), 14 ≤ ↑i → ↑i < 20 → y.regs i = x.regs i) ∧ (∀ r < x.regs modulus, ∀ k < C r ⌈/⌉ x.regs capacity, y.mem (x.regs dst + 3 * (before C (x.regs capacity) r + k)) = r ∧ y.mem (x.regs dst + 3 * (before C (x.regs capacity) r + k) + 1) = x.regs queries + 2 * r * (x.regs size * x.regs size) + 2 * (k * x.regs capacity) ∧ y.mem (x.regs dst + 3 * (before C (x.regs capacity) r + k) + 2) = min (x.regs capacity) (C r - k * x.regs capacity)) ∧ ∀ (a : ℕ), ¬(x.regs dst ≤ a ∧ a < x.regs dst + 3 * y.regs written) → y.mem a = x.mem a

Read the actual count table and concatenate every class's nonempty chunks. The controller receives no prefix sums. Both source blocks lie before dst; all other memory is preserved. The charged bound excludes halt.