Docs

Getting Started With ZeroProofML

ZeroProofML v0.5.1 is the Signed Common Meadow (SCM) release. It models singularities as an explicit bottom value, ⊥, and carries that decision through training, inference, export, and monitoring with masks instead of hidden guard branches.

Use this page to install the package, run the smallest examples, and choose the right next guide.

Installation

Create a virtual environment and install the backend you plan to use:

python -m venv .venv
source .venv/bin/activate

pip install "zeroproofml[torch]"

Optional extras:

pip install "zeroproofml[jax]"
pip install "zeroproofml[viz]"
pip install "zeroproofml[interactive]"

For a source checkout:

pip install -e ".[dev,torch]"

zeroproofml.* is the canonical public namespace for v0.5.1 docs and examples. The older zeroproof.* namespace remains a supported compatibility import path, so existing integrations do not need an immediate rename.

First SCM Values

Scalar SCM helpers are useful for notebooks, tests, and explaining semantics:

from zeroproofml.scm.ops import scm_add, scm_div
from zeroproofml.scm.value import scm_bottom, scm_real

x = scm_real(3.0)
zero = scm_real(0.0)

print(scm_div(x, zero))        # SCMValue(⊥)
print(scm_add(scm_bottom(), x))  # SCMValue(⊥)

The important rule is simple: once a computation reaches ⊥, the bottom value is absorptive.

Tensor Workflows

Arrays and tensors do not store ⊥ in the payload. They use a pair:

  • payload: ordinary numeric values
  • bottom_mask: boolean mask where True means the sample is bottom

Example with NumPy vectorized SCM division:

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

num = np.array([1.0, 2.0, 3.0])
num_mask = np.array([False, False, False])
den = np.array([1.0, 0.0, 2.0])
den_mask = np.array([False, False, False])

payload, bottom_mask = scm_div_numpy(num, den, num_mask, den_mask)
assert bottom_mask.tolist() == [False, True, False]

Treat the mask as authoritative. Payload values where bottom_mask=True are implementation details and should not drive losses, metrics, or decisions.

Two Modes

ZeroProofML uses two complementary modes:

Mode Use it for Contract
Strict SCM Inference, validation, deployment, monitoring Decode (P, Q) and emit ⊥ when `
Projective training Learning rational heads near poles Train on smooth homogeneous tuples (P, Q), then decode strictly at the boundary

The guiding rule is:

Train on smooth projective or policy-regularized objects. Infer with strict SCM semantics.

Minimal Strict Inference

from zeroproofml.inference import InferenceConfig, strict_inference

cfg = InferenceConfig(tau_infer=1e-6, tau_train=1e-4)
decoded, bottom_mask, gap_mask = strict_inference(P, Q, config=cfg)

The stable inference tuple is always:

  • decoded: finite decoded payload when accepted
  • bottom_mask: authoritative reject/fallback mask
  • gap_mask: finite but near-threshold samples where tau_infer <= |Q| < tau_train

gap_mask is for monitoring and conservative routing. It is not another kind of bottom.

When you have the library checkout, start with these maintained examples:

python examples/01_quickstart.py
python examples/02_rational_layer.py
python examples/03_projective_mode.py
python examples/05_coverage_control.py
python examples/06_export_bundle.py
python examples/fru_strict_check_demo.py

They cover scalar SCM values, rational layers, projective heads, coverage-aware training, ONNX bundle export, and flattened strict checks for composed rational heads.

What Changed In v0.5.1

  • SCM is the core semantics: singular states collapse to a single ⊥.
  • Transreal tags such as +∞, −∞, and Φ are not part of the v0.5.1 core.
  • Tensor workflows use numeric payloads plus explicit masks.
  • ONNX bundles are the preferred deployment artifact; TorchScript is a legacy compatibility path.
  • Optional provenance diagnostics can explain bottom decisions, but the stable deployment contract remains (decoded, bottom_mask, gap_mask).

Next Steps