Native ExactTriangle splitting parameters

The program computes the existing integer parameters sOf, queryCap, pieceSize and numPieces. Both square roots call the charged native successive-squares program; all products, quotients and ceilings are native instructions. The modulus is supplied separately by the outer prime-selection host.

Main definitions

• Parameters.program: fixed fifteen-register parameter computation.

Main results

• Parameters.exec: exact outputs, explicit word fits, cost and an unchanged-memory frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.arg : Fin 15

Square-root input and arithmetic scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.root : Fin 15

Square-root result.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.size : Fin 15

Input matrix side.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.dimension : Fin 15

Target middle dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.divisor : Fin 15

Piece-size divisor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.middleRoot : Fin 15

Output floor square root of the middle dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.capacity : Fin 15

Output query chunk capacity.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.pieceLength : Fin 15

Output maximum piece length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.pieces : Fin 15

Output number of pieces.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.area : Fin 15

Square of the outer dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.one : Fin 15

Constant one, outside the square-root register bank.

def Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.squareRoot : WordRAM.Code WordRAM.Basis.standard 15

Reused charged integer square root.

def Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.between : WordRAM.Code WordRAM.Basis.standard 15

Runtime arithmetic between the square roots.

def Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.finish : WordRAM.Code WordRAM.Basis.standard 15

Both natural ceilings use the existing (a+b-1)/b convention, including zero divisors.

def Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.program : WordRAM.Code WordRAM.Basis.standard 15

Fixed code; only the square-root loops depend on the runtime inputs.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.program_fixed : program.size ≤ 64 ∧ ¬program.ReadsWidth

Fixed native code and no physical-width reads.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Parameters.exec {w : ℕ} (x : WordRAM.Data 15) (hD : WordRAM.Fits w (4 * x.regs dimension + 4)) (hN : WordRAM.Fits w (4 * (x.regs size * x.regs size * (x.regs size * x.regs size)) + 4)) (hB : WordRAM.Fits w (ExactTriangle.sOf (x.regs dimension) + x.regs divisor)) (hH : WordRAM.Fits w (x.regs size + ExactTriangle.pieceSize (x.regs dimension) (x.regs divisor))) : ∃ (y : WordRAM.Data 15), WordRAM.ExecWithin w program x y (5 * ExactTriangle.sOf (x.regs dimension) + 5 * ExactTriangle.queryCap (x.regs size) (x.regs dimension) + 27) ∧ y.regs middleRoot = ExactTriangle.sOf (x.regs dimension) ∧ y.regs capacity = ExactTriangle.queryCap (x.regs size) (x.regs dimension) ∧ y.regs pieceLength = ExactTriangle.pieceSize (x.regs dimension) (x.regs divisor) ∧ y.regs pieces = ExactTriangle.numPieces (x.regs size) (x.regs dimension) (x.regs divisor) ∧ y.regs size = x.regs size ∧ y.regs dimension = x.regs dimension ∧ y.regs divisor = x.regs divisor ∧ y.mem = x.mem

Compute the finite splitting parameters from actual runtime dimensions. The two explicit ceiling-addition fits cover their temporary sums, and the fourth-power bound covers the square formed before dividing by D. The final halt is excluded.