ZeroProofML 0.6.0 is a hardening release for strict inference. It does not add a new application domain or public integration. The changes are concentrated around ⊥: how bottom results are classified, how non-finite payloads are routed, how simplification is constrained, and how projective thresholds are interpreted.

The 0.5.x line made deployment outputs easier to inspect through export bundles, validation reports, and deployment handoff. The 0.6.0 line makes the corresponding runtime contract more explicit. The operational question is no longer only whether an entry bottomed, but whether the bottom came from a runtime fault, a semantic threshold, or both.

Fault, Semantic, or Mixed Provenance Is Stable

In v0.5.x, the fault/semantic provenance split was still experimental. In v0.6.0, eager strict-inference results expose fault_mask, semantic_bottom_mask, and bottom_provenance as stable attributes. Three-field unpacking remains (decoded, bottom_mask, gap_mask), so existing callers that use the merged mask keep the same basic result shape.

The split masks are provenance annotations, not a replacement for bottom_mask. They are also not guaranteed to be disjoint. A sample can satisfy both a runtime-fault route and an explicit semantic threshold; in that case both split masks are set and bottom_provenance records MIXED. The merged relation remains:

bottom_mask = fault_mask | semantic_bottom_mask

Deployment code can choose the level it needs: bottom_mask for the conservative merged contract, the split masks for policy routing, or bottom_provenance for reporting. DOSE and reference robotics workflows already consume the split routing and now use stable attributes without an experimental flag.

Non-Finite Payloads Fail Closed

Strict inference now treats every non-finite P or Q payload as a fault bottom. When validity factors are supplied, non-finite factor values follow the same fail-closed route. Classification uses isfinite, not only isnan, so NaN, +Inf, and -Inf are invalid decoded payloads rather than semantic values.

Decoded bottom payloads remain sentinels. Bundle smoke-test parity compares decoded values only for non-bottom entries after validating bottom_mask. Consumers must honor the masks instead of reading decoded NaN values as model output. The v0.6.0 contract tests cover decoded-only consumers, bottom-mask-only consumers, and fault-mask-only consumers.

Censored-direction orientation must be carried through finite side channels, weak-sign or projective representations, or direction heads. It must not be inferred from IEEE infinity signs. Projective heads also expose bottom capability: if training data contains bottom labels that a configured head cannot reach under tau_infer, SCMTrainer raises unless allow_bottom_unreachable=True is passed.

Simplification Modes Are Explicit

Fracterm and FRU flattening now distinguish strict SCM simplification from field-rational simplification through the public SimplificationMode alias. Field-rational rewriting is the usual algebra of fields, but it can cancel denominator conditions that strict bottom-preserving semantics must retain. For that reason, it is available only through an explicit simplification_mode="field_rational" opt-in and is documented as unsafe for strict bottom-preserving pipelines.

The default path remains strict. It keeps flattening uncancelled where required and carries divisor denominator factors through division. Strict flattening refuses configured depth and degree-bound violations instead of using field-rational rescue rewrites. Strict cancellation refuses symbolic factor cancellation unless the factor is a safe numeric constant or is covered by a proven or declared nonzero assumption.

Pure strict Fracterm artifacts and guarded strict FlattenedFRU artifacts now carry explicit strict-preserving target tags. Public FRU structural validity-factor provenance remains experimental. Common-meadow anchor identities are documented and tested as semantic checks, not as required emitted normal forms.

Projective Gauge Conventions Are Named

A projective head predicts ⟨N,D⟩ up to scale. Any threshold on |Q| therefore depends on a scale convention. v0.6.0 makes that convention explicit through the public GaugePolicy enum and the opt-in ProjectiveNormalize(...) helper.

The supported conventions are canonical_denominator, unit_l2_projective, and angular_unit_circle, with canonical_denominator recorded as the default. The design-review note compares these conventions without changing strict-inference behavior. Post-hoc tau_infer sweeps over cached |Q| distributions remain valid for the head and magnitude convention that produced those distributions; they should not be treated as gauge-independent thresholds.

Numerical Hazards Are Monitor-Only

Finite but small denominators are no longer folded into fault_mask. The new numerical_hazard_threshold is monitor-only metadata. It is surfaced through the numerical_hazard_rate axis on StrictInferenceMonitor and strict_inference_rates(...), and it does not contribute to bottom_mask, fault_mask, or semantic_bottom_mask unless a consumer separately promotes that diagnostic.

The old provenance_fault_threshold name is deprecated but still accepted as an alias. Operationally, fault_rate, semantic_bottom_rate, and finite-hazard alerts should be thresholded separately. Frequent faults from a strict-flattened head indicate implementation hygiene issues, while an intentional IEEE-arithmetic head may use fault_mask as its correct fail-closed bottom route.

Training Defaults

sign_consistency_loss and SCMTrainingLoss are singular-only by default when mask_singular is omitted, selecting entries with abs(Y_d) <= epsilon_sing. implicit_loss(...) and implicit_loss_jax(...) now default to detach_scale=False, while detach_scale=True remains available as the legacy shrink heuristic. margin_loss adds an opt-in reduction="conditional" mode; the default remains the population-style masked batch mean.

The release also adds soft_coverage_loss(...) as a differentiable under-coverage surrogate and lift_semantic_targets(...) / SemanticTargets for explicit target lifting from finite, bottom, censored, domain-invalid, missing, and fault status labels. Sentinel-based lift_targets(...) remains available as the legacy/simple path for NaN/Inf projective targets.

Upgrade Notes

Most v0.6.0 changes are additive, but strict-mode flattening can change masks at singular edge cases and can refuse expressions that field-rational simplification previously accepted. Existing exported bundles continue to validate under their recorded schema and metadata, including strict_inference_schema_version, strict_inference_exports, and the recorded inference-output schema sidecar. They are not silently reinterpreted under the hardened v0.6.0 schema.

The provenance metadata sidecar is now inference_output_schema. The previous experimental_inference_output_schema key still validates as a deprecated alias and emits DeprecationWarning. 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.

After upgrading, rerun workflows that rely on strict flattening, strict-inference masks, or exported deployment bundles. The main reference checks are examples/fru_strict_check_demo.py, the RR-IK reference deployment, and the DOSE matrix and artifact path.

Operational Scope

v0.6.0 reduces ambiguity in strict-inference outputs. Bottoms now have stable fault, semantic, or mixed provenance. Non-finite payloads route through fault masks. Finite numerical hazards remain diagnostic unless a consumer explicitly promotes them. Field-rational simplification requires an explicit opt-in when it would weaken strict bottom-preserving semantics.

The release does not make old bundles adopt the new schema. It makes new strict-inference outputs easier to audit and harder to consume incorrectly.