Containerized LKB worker (Dockerfile.lkb), Postgres-backed queue, auto-deploy timer, and eigensolid convergence check module. Build: 0 jobs (no Lean build needed)
25 lines
650 B
R
25 lines
650 B
R
source("boot.R")
|
|
box_use(./b4)
|
|
box_use(../math/sidon)
|
|
|
|
#' @export
|
|
split_sidon_8 <- function(S) {
|
|
if (length(S) != 8) stop("Sidon 8-set must have exactly 8 elements")
|
|
S <- sort(S)
|
|
list(left = S[c(1, 3, 5, 7)], right = S[c(2, 4, 6, 8)])
|
|
}
|
|
|
|
#' @export
|
|
block_diag_8x8 <- function(left_block, right_block) {
|
|
result <- matrix(rep(list(b4$zero), 64), nrow = 8, ncol = 8)
|
|
for (i in 1:4) for (j in 1:4) {
|
|
result[[i, j]] <- left_block[[i, j]]
|
|
result[[i + 4, j + 4]] <- right_block[[i, j]]
|
|
}
|
|
result
|
|
}
|
|
|
|
#' @export
|
|
b4xb4_matrix <- function(word_left, word_right) {
|
|
block_diag_8x8(b4$burau_matrix(word_left), b4$burau_matrix(word_right))
|
|
}
|