Adjacency in prepared native ExactTriangle matrices #
These consumer lemmas connect actual prepared memory to the existing finite lopsided graph. The source prime window supplies the padding bound, and piece membership supplies each local coordinate. Neither is an additional layout certificate for the program.
Main results #
PreparationSpec.instance_adjacency: actual stored cells give the finite adjacency relations and zero padding, with piece coordinates and middle-width admissibility derived.
References #
The adjacency relations are those of the pinned Theorem 17 matrix construction. The composition with native memory readback is original.
theorem Cslib.Algorithms.WordRAM.ExactTriangle.PreparationSpec.instance_adjacency {n D g p : ℕ} (values : ℕ → ℤ) (wAB wBC wAC : Fin n → Fin n → ℤ) (hD : 16 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : p ∈ D.sqrtPrimeWindow) (hAB : ∀ (a b : Fin n), values (Matrix.pairIndex (a, b)) = wAB a b) (hBC : ∀ (b c : Fin n), values (n * n + Matrix.pairIndex (b, c)) = wBC b c) (hAC : ∀ (a c : Fin n), values (2 * (n * n) + Matrix.pairIndex (a, c)) = wAC a c) {initial y : WordRAM.Data 64} (h : Instances.Output n D g p values initial y) (idx : ExactTriangle.InstanceIndex p) (hidx : idx ∈ ExactTriangle.instanceIndices wAB D g p) :
have N := n * n;
have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => (values q % ↑p).toNat = rho) N;
have H := ExactTriangle.numPieces n D g;
have B := ExactTriangle.pieceSize D g;
have ord := ChunkCatalogue.before C (ExactTriangle.queryCap n D) ↑idx.1 + idx.2.1;
have base := y.regs Instances.output + (ord * H + idx.2.2) * (6 + 2 * (n * D));
let G := ExactTriangle.lopInstance wAB wBC wAC D g p idx;
(∀ (a b c : Fin n) (hc : c ∈ ExactTriangle.piece n D g idx.2.2) (label : Fin p),
have middle := ↑c % B * p + ↑label;
(y.mem (base + 6 + (↑a * D + middle)) = 1 ↔ G.adjA a (⟨c, hc⟩, label)) ∧ (y.mem (base + 6 + n * D + (middle * n + ↑b)) = 1 ↔ G.adjB (⟨c, hc⟩, label) b)) ∧ ∀ (a b : Fin n) (middle : Fin D),
min B (n - idx.2.2 * B) ≤ ↑middle / p →
y.mem (base + 6 + (↑a * D + ↑middle)) = 0 ∧ y.mem (base + 6 + n * D + (↑middle * n + ↑b)) = 0
The actual prepared matrix cells express the existing finite graph's adjacency, and the unused middle positions are zero. The prime-window and piece hypotheses discharge every padding and local-coordinate premise of the matrix-entry API.