Extended IEEE/Array Bridge Documentation (SCM)

Overview

ZeroProofML's bridge collapses IEEE NaN/Inf into the single SCM bottom element and keeps mask semantics aligned across NumPy, PyTorch, and JAX arrays. The helpers live in zeroproofml.utils.ieee_bridge for scalars and in zeroproofml.scm.ops for vectorised math.

Boundary rules. from_ieee/batch_from_ieee are the only supported entry points for non-finite IEEE inputs — they route NaN and ±Inf to at this named boundary. Bare SCMValue(float("nan")) construction raises ValueError, and finite scalar arithmetic that produces a non-finite result raises OverflowError. Vector-op masks (mask_x, mask_y) are keyword-only; positional forms, including the historical interleaved call, raise TypeError. The canonical exact-vs-finite numerical scope is in 01_scm_foundations.md.

Scalar Conversion

from zeroproofml.utils.ieee_bridge import from_ieee, to_ieee

scm_val = from_ieee(float("nan"))  # ⊥
print(scm_val.is_bottom)            # True
print(to_ieee(scm_val))             # nan

Use batch_from_ieee/batch_to_ieee when handling iterables.

NumPy and Torch Masks

Vectorised helpers take parallel arrays of payloads and boolean ⊥ masks. Operations propagate masks instead of materialising infinities:

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

payload = np.array([1.0, 0.0, -1.0])
mask = np.array([False, True, False])  # mark ⊥ locations

values, value_mask = scm_add_numpy(payload, payload, mask_x=mask, mask_y=mask)
quot, quot_mask = scm_div_numpy(payload, np.ones_like(payload), mask_x=mask, mask_y=np.zeros_like(mask))

Torch mirrors the same calling convention:

import torch
from zeroproofml.scm.ops import scm_mul_torch

x = torch.tensor([2.0, 0.0])
mask = torch.tensor([False, True])
prod, prod_mask = scm_mul_torch(x, torch.tensor([3.0, 4.0]), mask_x=mask, mask_y=mask)

All outputs return a (payload, mask) tuple. Masks stay boolean so they can be logged directly as coverage metrics. Since v0.6.1 vector helpers use one shared finalizer: incoming masks, zero/inverse-zero division, unsupported real domains, non-finite inputs, and backend NaN / ±Inf results are folded into the returned mask. Payload entries where mask=True are finite zero placeholders. Complex vector log / sqrt / pow follow the scalar boundary where supported, with pow limited to real exponents; complex vector pow exponents are refused. Real pow / log / sqrt reject unsupported domains into the mask. NumPy integer reciprocal promotes to floating output.

Projective Tuples

SCMRationalLayer exposes a bottom mask alongside its output so that singularities can be handled once at decode time:

from zeroproofml.layers import SCMRationalLayer
from zeroproofml.autodiff.policies import GradientPolicy

layer = SCMRationalLayer(1, 1, gradient_policy=GradientPolicy.PROJECT)
y, bottom_mask = layer(x)

This keeps the forward graph free of control flow and lets you decide whether to drop, clamp, or project ⊥ values in the trainer.

Design Notes

  • Single bottom element: NaN and ±∞ collapse to at the from_ieee boundary; there are no Transreal tags in v0.6.x.
  • Weak sign: Orientation can be recovered with zeroproofml.scm.sign.weak_sign after mapping finite values or bottom into SCM; non-finite payloads return bottom rather than a sign tag.
  • Deterministic masks: Vectorised ops derive masks from explicit domain checks and backend finiteness checks. Ideal common-meadow bottom is separate from finite IEEE overflow/domain faults; in v0.6.1 the vector shims classify those finite-backend faults into the mask and keep the payload finite.