IEEE / Array Bridge (SCM) — Summary

ZeroProofML v0.6.1 uses Signed Common Meadows (SCM): all domain errors and division-by-zero collapse to a single absorptive bottom element ⊥. There are no Transreal tags (+∞, −∞, Φ) in the core.

v0.6.1 boundary convention: from_ieee(NaN) and from_ieee(±Inf) are the only supported way to bring non-finite IEEE inputs into SCM — they route to ⊥ at this documented boundary. Direct SCMValue(float("nan")) / SCMValue(float("inf")) construction now raises ValueError, and finite-op-finite arithmetic that produces a non-finite result raises OverflowError. See 16_verification_report.md and the zeroproof/utils/ieee_bridge.py module docstring.

For the exact SCM vs finite IEEE execution boundary, including which overflows are masked and which paths are refused, see 01_scm_foundations.md.

The bridge story is therefore: - Scalars: map IEEE-754 NaN/±inf ↔ ⊥ - Arrays/tensors: carry a numeric payload plus an explicit boolean bottom mask

Scalar conversion (zeroproofml.utils.ieee_bridge)

Use this when you ingest external floats that may contain NaN/Inf.

from zeroproofml.utils.ieee_bridge import from_ieee, to_ieee

v = from_ieee(float("nan"))  # -> SCMValue(⊥)
assert v.is_bottom

out = to_ieee(v)             # -> nan (tooling-friendly sentinel)

Batch helpers are available for iterables: batch_from_ieee, batch_to_ieee.

Vectorised operations with masks (zeroproofml.scm.ops)

For numerical backends, SCM values are represented as: - payload: float/complex array (NumPy/JAX) or tensor (Torch) - mask: boolean array/tensor marking ⊥ positions

Vectorised operators propagate ⊥ by combining masks (and for division/inverse also checking for zeros). Masks are keyword-only: use mask_x=... and mask_y=.... The former positional and historical interleaved forms were removed in v0.7.0a1 and raise TypeError in both canonical and compatibility namespaces.

import numpy as np
from zeroproofml.scm.ops import scm_div_numpy

x = np.array([1.0, 2.0, 3.0])
x_mask = np.array([False, False, False])
y = np.array([1.0, 0.0, 1.0])
y_mask = np.array([False, False, False])

q, q_mask = scm_div_numpy(x, y, mask_x=x_mask, mask_y=y_mask)  # q_mask[1] == True (division by zero -> ⊥)

Backends: - NumPy: scm_*_numpy - PyTorch: scm_*_torch - JAX: scm_*_jax

All vectorised functions return (payload, mask). Since v0.6.1 the returned mask also absorbs unsupported real domains and backend non-finite results from finite IEEE execution; masked payload entries are finite zero placeholders. Complex vector pow accepts real exponents only; complex exponents are refused in v0.6.1.

Torch rational layers: bottom_mask as the SCM boundary

Torch SCM layers follow a single-check pattern: forward passes return a mask that you treat as ⊥ at the boundary (loss, logging, inference decode).

Example: SCMRationalLayer returns (output, bottom_mask) where bottom_mask flags denominator singularities. Since v0.6.1 the layer's forward substitutes safe operands before the division (and for sub-float64 inputs adds a promoted-float64 pre-division overflow check), so the autograd graph never sees a NaN/Inf division node; the torch.where below is a display convention, not a repair.

import torch
from zeroproofml.layers import SCMRationalLayer

layer = SCMRationalLayer(1, 1)
x = torch.tensor([-1.0, 0.0, 1.0])
y, bottom = layer(x)
decoded = torch.where(bottom, torch.full_like(y, float("nan")), y)

Design choices

  • ⊥ maps to IEEE NaN on export (to_ieee) so downstream tooling (NumPy/Pandas/metrics) can treat it as “invalid”.
  • Array/tensor SCM semantics stay compiler-friendly: the “special value” is in the mask, not in the payload.
  • Coverage metrics are naturally expressed as 1 - bottom_mask.float().mean().