Signed Common Meadows (SCM) Primer

ZeroProofML v0.6.1 grounds its semantics in signed common meadows: a field of characteristic 0 extended with a total inverse and a single absorptive bottom element (⊥). Division by zero yields ⊥, which then absorbs addition and multiplication, allowing singularities to propagate without ad-hoc guard branches.

Weak Sign Structure

SCM augments the meadow core with a sign operator that preserves orientation even when magnitudes blow up. For real inputs the operator is 4-signed; for complex inputs it projects finite nonzero values onto the unit circle, returning ⊥ unchanged and locking the last valid orientation when approaching the origin. This weak-sign contract does not require strict inference to accept IEEE +inf / -inf as valid decoded payloads. This weak-sign construction makes the library usable for higher-dimensional robotics where ordered-field assumptions break down.

Bottom-Aware Training and Inference

The SCM core already ensures total arithmetic, but training benefits from explicit handling of singular paths. Gradient policies clamp, reject, or project gradients that traverse ⊥ during the backward pass, while the forward graph stays faithful to the algebra. The optional projective extension lifts select subgraphs to homogeneous tuples (N, D), giving the optimizer a smooth manifold and delaying any ⊥ instantiation to the boundary decode step. The guiding rule is:

Train on smooth (policy- or projective-regularized) objects; infer on strict SCM semantics.

Boundary examples and excluded cases

  • Field cancellation is not strict SCM equivalence. x/x may agree with 1 for nonzero field values, but at x = 0 the strict SCM expression is bottom. Likewise 1/(1/x) must retain the original bottom-producing support; the symbolic check registered as THY-001 records these boundaries.
  • IEEE non-finites are not algebraic bottom by accident. Direct scalar construction with NaN or infinity is refused. Only the explicitly named IEEE bridge classifies those carriers as bottom, and finite arithmetic overflow is a numerical fault rather than a covert algebraic conversion.
  • A strict threshold is not a gauge-invariant safety certificate. Raw projective |Q| scores can vary with representation. v0.6.x therefore treats deployment scoring as gauge-dependent and does not claim universal calibration across heads or normalization conventions.
  • Masks represent distinct operational facts. Bottom, semantic bottom, runtime fault, and observation/censoring information must not be conflated. The current mask contract is documented at the inference boundary; the richer taxonomy remains a future design task rather than an established theorem.

Further Reading