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 finite values keep orientation; ⊥ stays ⊥; non-finite payloads return bottom rather than an orientation tag Rational heads can preserve direction near singularities without treating IEEE infinities as carriers
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.

Strict inference classifies non-finite payloads using isfinite, not only isnan. NaN, +Inf, and -Inf route to fault_mask (a fail-closed bottom) rather than becoming semantic values. Censored direction must be carried in a finite side channel, weak-sign representation, angular head, or an auxiliary direction head, not inferred from the IEEE infinity sign of an overflowed scalar.

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.

Gauge Conventions

A projective head predicts ⟨N, D⟩ up to scale, so any threshold on |Q| depends on a scale convention. v0.6.0 names that choice through the public GaugePolicy enum and opt-in ProjectiveNormalize(...) helper:

  • canonical_denominator: keep the denominator magnitude exactly as trained (default).
  • unit_l2_projective: normalize (P, Q) by sqrt(P^2 + Q^2) before thresholding.
  • angular_unit_circle: record the unit-circle convention used by angular heads.

Post-hoc tau_infer sweeps over cached |Q| distributions stay gauge-correct only for the head and magnitude convention that produced those distributions.

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.

For complex values, weak_sign projects finite non-zero payloads onto the unit circle and returns bottom for non-finite payloads. IEEE infinity signs are not carriers.

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 through a finite direction head

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.6.0 implementation supports constants, variables, sparse polynomial numerators and denominators, and shallow expressions built from +, *, and /. Depth and degree growth are capped (L <= 5, with a 16 * d degree multiplier bound where d = max(d_p, d_q)) so flattening remains an audit/export tool rather than a per-step training operation.

Strict flattening refuses configured depth and degree-bound violations rather than falling back to field-rational rewrites. It also keeps divisor denominators as bottom-producing factors through division.

Strict vs Field-Rational Simplification

v0.6.0 exposes a public SimplificationMode alias:

  • scm_strict (default): keeps bottom-preserving semantics. Symbolic factor cancellation is limited to safe numeric constants and monomial factors covered by proven or declared nonzero assumptions.
  • field_rational: explicit unsafe opt-in that uses ordinary field algebra (a/b)/(u/v) = av/(bu). This can cancel denominator conditions that strict SCM must retain and is documented as unsafe for strict bottom-preserving pipelines.

Common-meadow identities such as x/x = 1 + 0/x and 1/(1/x) = x + 0/x are semantic anchors: canceling them to 1 or x erases the bottom at x = 0. Strict simplifiers keep the anchor, not necessarily one canonical normal form.

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.6.0. 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; authoritative
fault_mask Bottom from non-finite P/Q/validity payload (fail-closed)
semantic_bottom_mask Bottom from a finite threshold trigger (`
bottom_provenance Integer codes for NONE, FAULT, SEMANTIC, MIXED
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