Docs

SCM Foundations

Signed Common Meadows give ZeroProofML a total arithmetic for singular functions. Division by zero does not throw, branch into hand-written guards, or create IEEE NaN/Inf inside the model. It yields one explicit absorptive element: ⊥.

Core Rules

Concept Rule Practical meaning
Total inverse 0^-1 = ⊥ Division is defined everywhere
Absorption x + ⊥ = ⊥, x * ⊥ = ⊥ Once a path is bottom, downstream math stays bottom
Weak sign Non-zero values keep orientation; ⊥ remains ⊥ Rational heads can preserve direction near singularities
Explicit masks Tensors carry (payload, bottom_mask) Masks, not payload sentinels, drive decisions

SCM is intentionally stricter than "replace bad values later." It keeps singularity information in the computation contract from the first domain error through export and monitoring.

Bottom Versus IEEE Values

At package boundaries, ZeroProofML can bridge between IEEE floats and SCM values:

from zeroproofml.utils.ieee_bridge import from_ieee, to_ieee

v = from_ieee(float("inf"))
assert v.is_bottom

nan = to_ieee(v)

Use the bridge at ingress and egress. Inside SCM-aware code, prefer explicit masks so you do not accidentally lose whether a value was rejected, censored, or merely represented as NaN for external tooling.

Payload Plus Mask

For NumPy, PyTorch, and JAX workflows, every vectorized SCM operation follows the same shape:

(payload_a, mask_a), (payload_b, mask_b) -> (payload_out, mask_out)

mask_out=True if an input was bottom or if the operation creates a new singular state, such as division by zero. Coverage is therefore direct:

coverage = 1.0 - bottom_mask.float().mean()

Projective Tuples

Rational models often learn more reliably when the head emits a homogeneous tuple:

(P, Q) represents P / Q

Finite values decode as P / Q. Bottom appears only at the strict boundary:

|Q| < tau_infer -> ⊥

During training, detached renormalization keeps tuples bounded:

(P, Q) <- (P, Q) / stop_gradient(sqrt(P^2 + Q^2) + gamma)

This avoids a brittle training process that instantiates bottom values at every near-pole batch.

Weak Sign And Orientation

Near a pole, magnitude alone is not enough. A rational head may need to distinguish which side of the singularity it approached. ZeroProofML uses weak-sign structure and sign-consistency losses to preserve orientation in projective tuples.

This matters for robotics, censoring, and other regimes where "invalid" still carries useful direction:

  • a solver fallback may depend on which side of a joint singularity was reached
  • a censored prediction may need a below-limit versus above-limit class
  • an infinite target can be meaningful if the orientation is stable

Fracterm Flattening

Common meadow theory allows rational expressions to be flattened into one P(x) / Q(x) term. ZeroProofML uses this locally for Fused Rational Units (FRUs), not as a whole-network symbolic compiler.

The practical reason is deployment clarity:

  1. compose shallow rational stages
  2. flatten the small head into one final (P, Q) pair
  3. check the final denominator once during strict inference

The v0.5.1 implementation supports constants, variables, sparse polynomial numerators and denominators, and shallow expressions built from +, *, and /. Depth and degree growth are capped so flattening remains an audit/export tool rather than a per-step training operation.

Use projective training for optimization. Use flattening after training when you need a stable artifact for denominator checks, provenance review, or export validation.

Precision Notes

There is no global float64 enforcement layer in v0.5.1. Precision is still important near denominators:

  • Prefer torch.float64 for rational heads in near-singular robotics, stiff physics, and similar workloads.
  • Tune SCMRationalLayer.singular_epsilon for forward denominator detection.
  • Tune tau_train_min, tau_train_max, and tau_infer separately; they serve different roles.
  • Avoid ad hoc nan_to_num calls inside SCM pipelines because they erase bottom-mask information.

Terms

Term Meaning
⊥ / bottom Absorptive singular state
bottom_mask Boolean tensor marking bottom samples
gap_mask Finite samples in `tau_infer <=
Coverage Fraction of samples that are not bottom
Projective tuple Homogeneous (P, Q) carrier for rational values
Strict decode Deployment-time conversion from (P, Q) to finite payload plus masks