Docs

Getting Started With ZeroProofML

ZeroProofML 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.6.0 docs and examples. The older zeroproof.* namespace remains a supported compatibility import path through the roadmap's next major milestone, so existing integrations do not need an immediate rename.

For paper-exact reproduction, keep using the v0.4.3 release tag or zeroproofml==0.4.3. v0.6.x is the active development line.

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)
result = strict_inference(P, Q, config=cfg)

decoded, bottom_mask, gap_mask = result
fault_mask = result.fault_mask
semantic_bottom_mask = result.semantic_bottom_mask
bottom_provenance = result.bottom_provenance

The stable three-field tuple is always:

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

The eager result object also carries stable provenance detail:

  • fault_mask: non-finite P/Q payload or non-finite validity factor
  • semantic_bottom_mask: finite denominator triggered a strict threshold
  • bottom_provenance: integer codes (NONE, FAULT, SEMANTIC, MIXED)

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.6.0

  • Bottom provenance is stable: fault_mask, semantic_bottom_mask, and bottom_provenance are now guaranteed result attributes, not experimental opt-ins.
  • Non-finite P, Q, and validity factors fail closed to fault_mask; censored direction must come from a finite side channel, not IEEE +inf / -inf.
  • Fracterm/FRU flattening exposes a public SimplificationMode. simplification_mode="field_rational" is an explicit unsafe opt-in; strict is the default.
  • Projective gauge conventions are named: GaugePolicy (canonical_denominator, unit_l2_projective, angular_unit_circle) plus the opt-in ProjectiveNormalize(...) helper.
  • Finite numerical hazards are monitor-only: numerical_hazard_threshold surfaces through numerical_hazard_rate and does not fold into fault_mask.
  • Loss defaults changed: sign_consistency_loss is singular-only when mask_singular is omitted, implicit_loss(..., detach_scale=False) is default, and margin_loss gets an opt-in reduction="conditional" mode.
  • New training helpers: soft_coverage_loss(...), lift_semantic_targets(...), and SemanticTargets for explicit finite/bottom/censored/domain-invalid/missing/fault labels.
  • Bundle metadata sidecar renamed to inference_output_schema; the old experimental_inference_output_schema remains a deprecated alias.

Next Steps