Reference · Algorithm guarantees

rainbow.algorithms.proofs.latin-hypercube

Algorithm guaranteessrc/rainbow/algorithms/proofs/latin_hypercube.clj3 definitions, 4 theorems

AHoF O59 Latin Hypercube Sampling: a space-filling design that draws exactly n sample points across any number k of dimensions, in contrast to the full factorial design (O58) whose size grows as the product of per-dimension level counts. LHS partitions each of the k dimensions into n equal-probability strata and places one point per stratum row, so: sample-count n k = n (n evaluations, independent of k) strata-per-dimension n k = n (each dimension is split into n strata) total-strata n k = n * k (n strata across each of k dimensions) The defining efficiency property is that the number of objective evaluations is n regardless of dimension -- linear, where full factorial is exponential. These are exact natural-number counts; the concrete stratum boundaries and the Latin-square permutation that assigns points to strata stay an executable concern. What is proved here is the sampling-cost arithmetic, reduced by reflexivity. Scope (measured by the kernel): this module has 2 worked instances (statements about specific values) and 2 definitional unfoldings (true by unfolding a definition). None of its theorems is a guarantee about the algorithm for all inputs; `lein verify rainbow.algorithms.proofs.latin-hypercube` prints this classification.

latin-hypercube/sample-count :
  (x₁ x₂ : ℕ)
  → ℕ

latin-hypercube/strata-per-dimension :
  (x₁ x₂ : ℕ)
  → ℕ

latin-hypercube/total-strata :
  (x₁ x₂ : ℕ)
  → ℕ

latin-hypercube/sample-count-is-n :
  (n k : ℕ)
  → latin-hypercube/sample-count n k = n

latin-hypercube/total-strata-is-product :
  (n k : ℕ)
  → latin-hypercube/total-strata n k = nat/multiply n k

latin-hypercube/sample-count-4x3-example :
  → latin-hypercube/sample-count 4 3 = 4

latin-hypercube/total-strata-4x3-example :
  → latin-hypercube/total-strata 4 3 = 12