mod laws

module laws

Law-witness helpers and the LawViolation diagnostic type. Runtime witnesses + the LawViolation error returned by SaVariant::checked when a tuple of components fails one of the four IISE-manuscript composition laws.

SaVariant::checked_with_sweep exercises the executable behavior of each law on n_samples random inputs rather than trusting Boolean witness methods alone.

Functions

fn sweep_accept_monotone_in_temp<A: AcceptRule<f64>>(accept: &A, n_samples: usize, seed: u64) -> Result<(), LawViolation>

Witnesses L4 by sampling uphill moves at paired temperatures and checking that acceptance probability is non-decreasing in temperature.

fn sweep_cooling_monotone<C: Cooling<f64>>(cool: &C, n_epochs: usize) -> Result<(), LawViolation>

Witnesses L4 (cooling non-increasing in epoch) on a Cooling<f64> by computing T(0), T(1), ..., T(n_epochs - 1) and checking each successive pair.

fn sweep_downhill_accepts<A: AcceptRule<f64>>(accept: &A, n_samples: usize, seed: u64) -> Result<(), LawViolation>

Witnesses L3 (downhill always accepts) on an AcceptRule<f64> by sampling n_samples random (delta_e <= 0, temp > 0) pairs and checking accept_prob == 1.0 for each. Uses seed for reproducibility.

fn sweep_move_support<M, N>(mover: &M, neigh: &N, dim: usize, bound: f64, n_samples: usize, seed: u64) -> Result<(), LawViolation>
where
    M: MoveKernel<f64>,
    N: Neighborhood<f64>

Witnesses L2 by drawing proposals from sampled feasible states and checking membership before any objective evaluation. The bounding cube is a validation domain supplied by the caller, not a proof over all states.

fn sweep_neighborhood_symmetric<N: crate::neigh::Neighborhood<f64>>(neigh: &N, dim: usize, bound: f64, n_samples: usize, seed: u64) -> Result<(), LawViolation>

Witnesses L1 (neighborhood symmetry) on a Neighborhood<f64>` by sampling n_samples random (i, j)` position pairs in the supplied bounding box and checking ``contains(i, j) == contains(j, i).

Enums

enum LawViolation

A law-violation diagnostic surfaced by SaVariant::checked / SaVariant::checked_with_sweep.

EmptySweep

Sampled validation requires at least one sample per executable law.

Symmetry

L1: is_symmetric() returned false on the supplied Neighborhood.

SymmetrySweep

L1 (sweep): proptest sampler caught a non-symmetric pair.

i: Vec<f64>

First witness point.

j: Vec<f64>

Second witness point.

SupportEscape

L2: MoveKernel::supports_in(neigh) returned false.

SupportEscapeSweep

L2 (sweep): a sampled proposal escaped the neighborhood.

from: Vec<f64>

Feasible state from which the proposal was drawn.

to: Vec<f64>

Proposal outside the declared neighborhood.

temp: f64

Positive proposal temperature.

NoFeasibleSweepState

The supplied validation cube contained no sampled feasible state.

DownhillNotAccepted

L3 (sweep): accept_prob(delta, T) != 1 for some delta <= 0.

delta_e: f64

Witness energy delta (<= 0).

temp: f64

Witness temperature.

p: f64

Reported acceptance probability (should be 1).

NonMonotoneCooling

L4: Cooling::is_monotone() returned false.

NonMonotoneCoolingSweep

L4 (sweep): cooling schedule caught growing in epoch.

k1: usize

Earlier epoch.

k2: usize

Later epoch.

t1: f64

Temperature at k1.

t2: f64

Temperature at k2 (which exceeded t1).

NonMonotoneAcceptInTemp

L4 (sweep): accept_prob(delta, t1) exceeds accept_prob(delta, t2) with t1 < t2.

delta_e: f64

Witness energy delta (> 0).

t1: f64

Lower temperature.

p1: f64

Acceptance probability at t1.

t2: f64

Higher temperature.

p2: f64

Acceptance probability at t2 (should be >= p1).