Mathematical Framework for Strict SCM Inference¶

This note states the mathematical contract implemented by ZeroProofML's current SCM hardening work (v0.6.1). It complements the SCM primer and fracterm-flattening note with the concrete strict-inference and flattening boundary rules.

1. Carrier and Total Arithmetic¶

The base semantic object is a field-like carrier K extended with one absorptive bottom element:

K_bot = K union {bot}

For ordinary payloads, K is modeled by finite real or complex numerics. IEEE NaN, +Inf, and -Inf are not carrier elements. At the strict inference boundary they are mapped to bottom through the fault axis.

The scalar SCM operations are total:

x + bot = bot
x * bot = bot
-bot = bot
x / bot = bot
bot / x = bot
x / 0 = bot
x / y = ordinary field quotient when x,y in K and y != 0

The implementation-level scalar witness is SCMValue: the is_bottom flag is the semantic source of truth, and the payload is meaningful only when that flag is false. Array and tensor paths use the same idea as (payload, bottom_mask); payload values on masked entries are not semantic data.

Since v0.6.1, this contract is enforced at the construction and scalar-op boundaries: SCMValue.__post_init__ rejects non-finite payloads (NaN, ±Inf, complex components) with ValueError, and finite-op-finite scalar arithmetic that produces a non-finite result raises OverflowError. Non-finite IEEE inputs may only enter the SCM carrier through the named IEEE→SCM boundary zeroproofml.utils.ieee_bridge.from_ieee(...), which routes them to ⊥ explicitly.

2. Weak Sign and Orientation¶

The signed-common-meadow layer includes a weak sign/orientation operation. For finite nonzero real values it agrees with the ordinary sign; for finite nonzero complex values it projects to the unit circle. Bottom remains bottom.

Operationally, strict inference does not preserve orientation by accepting IEEE infinities as decoded scalar values. If a workflow needs orientation near a singular boundary, that orientation must come from a finite weak-sign side channel, an angular/projective head, a direction head, or typed semantic labels.

3. Projective Training, Strict Decoding¶

A projective tuple (P, Q) represents a candidate value P / Q. Training may use smooth projective or gauge-normalized carriers, but strict inference applies the SCM boundary rule:

decoded = P / Q when P,Q finite, |Q| >= tau_infer, and all V_i pass
decoded = NaN payload when bottom_mask is true

The payload NaN is only a transport sentinel. Consumers must use bottom_mask for accept/reject decisions.

Since v0.6.1, tau_infer and tau_train are re-validated through shared validators at every strict-inference boundary (InferenceConfig, decode_strict_censored_3way, TrainingConfig, validate_bundle): tau_infer must be finite and strictly positive; tau_train (if set) must be finite, strictly positive, and >= tau_infer. tau_infer = 0 is refused — the SCM boundary rule above is only meaningful when tau_infer > 0.

For optional training-gap diagnostics:

gap_mask = not bottom_mask and tau_infer <= |Q| < tau_train

gap_mask is monitor-only and does not imply bottom.

4. Stable Strict-Inference Mask Contract¶

The stable eager Python result unpacks as:

(decoded, bottom_mask, gap_mask)

It also exposes stable attributes:

fault_mask
semantic_bottom_mask
bottom_provenance

Schema-v2 ONNX bundles expose the canonical six-output order:

decoded
bottom_mask
gap_mask
fault_mask
semantic_bottom_mask
bottom_provenance

The runtime mask equations are:

fault_mask =
    not finite(P)
 OR not finite(Q)
 OR any_i not finite(V_i)

semantic_bottom_mask =
    |Q| < tau_infer
 OR any_i |V_i| < tau_i

bottom_mask = fault_mask OR semantic_bottom_mask

The masks are not required to be disjoint. A sample with both a non-finite payload and a below-threshold denominator sets both split masks. gap_mask remains disjoint from bottom_mask.

The provenance enum is a compact, non-lossy summary:

0 = NONE      when not fault and not semantic
1 = FAULT     when fault and not semantic
2 = SEMANTIC  when semantic and not fault
3 = MIXED     when fault and semantic

Finite tiny-denominator hazards above tau_infer are not faults. They may be reported through a separate numerical-hazard monitor, but they do not alter bottom_mask, fault_mask, or semantic_bottom_mask.

5. Pure Strict Fracterms¶

For small rational expressions, a pure strict Fracterm stores one pair (P, Q). All bottom-producing denominator conditions must remain represented inside that pair unless a nonzero condition is proven or explicitly declared as a caller contract.

For two fracterms A = a/b and B = u/v, strict operations use:

A + B = (a*v + u*b) / (b*v)
A * B = (a*u) / (b*v)
A / B = (a*v^2) / (b*u*v)

The division rule is the critical common-meadow-preserving rule: v = 0 makes the divisor u/v bottom, so the outer division must also bottom. The ordinary field quotient (a*v)/(b*u) is valid only under the explicit field_rational opt-in and is unsafe for strict bottom semantics.

This explains the standard singularity anchors:

x/x       behaves like 1 + 0/x, not bare 1
1/(1/x)   behaves like x + 0/x, not bare x
0/x       bottoms at x = 0 unless x is known nonzero

These identities are semantic anchors. The simplifier does not need to emit those exact normal forms; it must emit a representation that bottoms on the same strict singular assignments.

6. Guarded Strict FRU Representations¶

FlattenedFRU may use a reduced finite payload plus load-bearing validity factors:

(P, Q, V_1, ..., V_n)

Acceptance requires all checks to pass:

finite(P)
finite(Q)
|Q| >= tau_infer
for all i: finite(V_i) and |V_i| >= tau_i

Examples of guarded strict payloads are:

x/x          -> (1, 1, {x})
1/(1/x)      -> (x, 1, {x})
0/x          -> (0, 1, {x})
(a/b)/(u/v)  -> (a*v, b*u, {v})

The validity factors are internal semantics, not optional audit sugar. Public structural validity provenance remains experimental, but guarded FRU correctness depends on evaluating every retained factor. Multiplying factors into one scalar gate is not the contract because it corrupts source provenance and threshold calibration.

Since v0.6.1, the FRU operational surface adds two refusals that guard the flatten path before it can silently drift outside the semantic model:

• evaluate_fru_expression(...) defaults to strict=True and refuses floating coefficients / assignments with FloatingCoefficientRefusal (a ValueError). Operational callers must opt in with strict=False, which emits a RuntimeWarning naming every offending float. The flatten path is operational only — not a proof or exact-symbolic oracle.
• FRUExpression.flatten() runs a memoized DAG walk to bound pre-expansion work and raises FRUResourceRefusal(RuntimeError) when the estimated work exceeds FLATTEN_MAX_WORK = 100_000 or the per-term product exceeds FLATTEN_MAX_TERM_PRODUCT = 10_000. Callers may raise the budget explicitly with max_flatten_work / max_term_product after measuring cost.

7. Domain Assumptions¶

Domain assumptions such as ("x", "nonzero") are caller contracts. They may justify local strict simplification, for example:

x/x -> 1/1 under assumption x != 0
0/x -> 0/1 under assumption x != 0

They are not runtime guards. If deployment data violates a declared nonzero assumption, the artifact is outside its declared semantic guarantee unless a separate validator is installed.

8. Degree Budgets¶

Local flattening is intentionally bounded. With seed degree d = max(deg(P), deg(Q)) and fused depth L, the guarded/field-style payload budget is:

guarded_bound(L, d) = 2^(L - 1) * d

Pure strict division can grow faster because division duplicates the divisor denominator:

D(A / B) <= D(A) + 2*D(B)
pure_strict_bound(L, d) = 3^(L - 1) * d

For a four-division chain after the seed, equivalently fused depth L = 5:

pure strict: 3^4 * 4 = 324
guarded:     2^4 * 4 = 64

If strict flattening exceeds configured bounds, the implementation must refuse or return an explicit audit-only unflattened record. It must not silently rescue the expression with field-rational simplification.

9. Typed Semantic Targets and Losses¶

Typed targets distinguish semantic labels before tensor sentinels are involved. The recommended target lifting path accepts labels such as:

finite
bottom
censored_below
censored_above
domain_invalid
missing
fault

This avoids treating NaN or Inf as the source of semantic truth. It also allows bottom labels to carry fault/semantic kind and optional orientation metadata.

Losses and trainer checks follow the same contract:

• bottom-capability checks raise when a head cannot enter the strict bottom region but bottom labels are present. Since v0.6.1 this is a structural guarantee only (e.g. softplus / anchor floors); the historical tau_infer = 0 fail-open route to "unreachable by construction" is refused up-front by the shared threshold validator and is no longer available.
• margin loss distinguishes population and conditional reductions;
• singular-orientation loss is not a generic finite-regression constraint;
• soft coverage is a differentiable training surrogate, while strict inference remains hard.

10. Mechanized Checks¶

The lightweight verification artifacts live in:

tools/verify_mathematical_framework.py
tools/mathematical_framework_check.lean

The SymPy checker verifies the field-of-fractions equalities and denominator support facts that ordinary algebra can see:

• strict division equals the ordinary field quotient away from singularities;
• strict division retains the divisor denominator factor that field reduction erases;
• x/x, 1/(1/x), and 0/x retain the singular support needed for SCM bottom behavior;
• guarded FRU examples keep erased denominator factors as validity factors;
• the degree-budget calibrations compute to 324 and 64.

The Lean checker avoids external mathlib dependencies and verifies discrete framework invariants:

• bottom_mask = fault_mask OR semantic_bottom_mask;
• gap_mask is disjoint from bottom_mask;
• the NONE, FAULT, SEMANTIC, and MIXED provenance encoding round-trips to the split masks;
• strict support tracking keeps the divisor denominator where field support does not;
• the degree-budget recurrence calibrations match the documented numbers.

These checks do not constitute a full formalization of common meadows. They are sanity checks for the equations and invariants that this implementation uses at the strict inference and flattening boundaries.