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 thefrom_ieeeboundary; there are no Transreal tags in v0.6.x. - Weak sign: Orientation can be recovered with
zeroproofml.scm.sign.weak_signafter 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.