Fracterm Flattening in ZeroProofML¶

Common meadow theory guarantees that any term over the signature can be flattened into a single rational function P(x)/Q(x). ZeroProofML adopts this result for Fused Rational Units (FRUs) to make singularity detection and policy selection predictable without expanding the entire network.

Engineering Scope¶

Local flattening only. To avoid degree explosion, flattening is restricted to small rational heads instead of whole models; the rest of the network stays in standard SCM or projective form.
Constant-time checks. By keeping the rational part flattened, we can decide whether a forward pass hits the ⊥-producing denominator with an O(1) check on Q_head, rather than walking each intermediate layer.
Projective compatibility. FRU outputs can be decoded either strictly into SCM values or as projective tuples (N, D) during training, keeping gradients smooth around poles.

Implementation Status¶

zeroproofml.scm.fracterm provides symbolic utilities for representing and simplifying small P/Q terms, with SimplificationMode = Literal["scm_strict", "field_rational"] defaulting to scm_strict. The strict representation is object-specific: Fracterm.strict_preserving_target is pure_strict_fracterm, so strict output keeps every bottom-producing condition inside one common-meadow-preserving (P, Q) pair.
zeroproofml.layers.fru now exposes a small typed FRU AST (FRUExpression, FRUConstant, FRUVariable, FRURational, FRUAdd, FRUMul, FRUDiv) plus FlattenedFRU, which flattens small symbolic heads into explicit P/Q pairs and records structural denominator provenance. FlattenedFRU.strict_preserving_target is guarded_strict_fru, so strict FlattenedFRU output may use a reduced finite payload when load-bearing validity factors are available.
zeroproofml.layers.fru.FractermRationalUnit still enforces degree-growth and depth constraints; its legacy flatten(...) helper validates precomputed coefficient lists, while flatten_expression(...) validates typed FRU expressions against the same bounds and can opt into an audit-only unflattened refusal record.

Current Utility Inventory¶

Utility	Current input model	Expression classes supported today	Notes
`zeroproofml.scm.fracterm.Polynomial`	Sparse multivariate polynomial terms built from `Polynomial.constant(...)`, `Polynomial.variable(...)`, `+`, and `*`	Numeric constants, single variables, monomials, and finite polynomial sums/products	There is no dedicated subtraction or power AST node; subtraction is encoded with negative coefficients and powers come from repeated multiplication.
`zeroproofml.scm.fracterm.Fracterm`	Symbolic rational terms built from `Fracterm.from_constant(...)`, `Fracterm.from_variable(...)`, direct `Fracterm(P, Q)` construction, and binary `+`, `*`, `/` composition	Already-flattened `P/Q` pairs plus shallow rational expressions assembled from constants, variables, polynomial numerators/denominators, addition, multiplication, and division	Default `flatten(...)` keeps strict SCM bottom factors intact, including the divisor denominator in division. `aggressive=True` and the registered `bergstra_tucker` symbolic simplifier require `simplification_mode="field_rational"` because they apply field-rational rules that can erase bottoms. There is no parser for generic expression trees and no support for transcendental or piecewise nodes.
`zeroproofml.layers.fru.FRUExpression.flatten(...)`	Typed FRU nodes (`FRUConstant`, `FRUVariable`, `FRURational`, `FRUAdd`, `FRUMul`, `FRUDiv`)	Small symbolic rational heads composed from constants, variables, explicit rational leaves, and binary `+`, `*`, `/` nodes	Returns `FlattenedFRU`, which carries the flattened `P/Q` pair plus experimental structural denominator provenance and optional `domain_assumptions`. Optional symbolic simplification delegates to `zeroproofml.scm.fracterm` and requires the same explicit unsafe mode.
`zeroproofml.layers.fru.FractermRationalUnit.flatten(...)` / `flatten_expression(...)`	Precomputed coefficient iterables or typed FRU expressions	Coefficient-list representations of an already flattened head, or a small typed FRU tree that should be flattened locally	Both helpers enforce FRU depth/degree bounds. They do not attempt whole-network or generic PyTorch graph lowering.

In short, the current flattening surface covers a small algebraic fragment: constants, variables, sparse polynomial numerators/denominators, and rational expressions formed by repeated use of +, *, and /. Anything outside that fragment still needs a separate lowering step before it can be passed into the fracterm helpers.

Structural Validity Provenance¶

FlattenedFRU.denominator_provenance is structural validity provenance from FRU flattening and is preserved for compatibility. The experimental FlattenedFRU.strict_validity_sources field records which symbolic denominator-bearing subexpression contributed each validity factor not already enforced by the reduced payload denominator. It remains experimental audit metadata with no defined promotion gate as a public trace. It does not inherit the historical Q2 downstream-benefit, overhead, repeatability, or non-regression thresholds; if a future consumer requests promotion, define a new structural-provenance gate at that time with fresh thresholds while using that Q2 pattern as precedent. Internally, those validity factors are still load-bearing for guarded strict FRU evaluation: a reduced payload is SCM-correct only when every erased bottom-producing factor is evaluated by the strict factorwise predicate. They are kept as source entries and are not collapsed into one scalar product for gating, because each factor carries its own threshold and provenance. Division provenance labels the divisor numerator and denominator separately as divisor_numerator and divisor_denominator so audits can distinguish both strict bottom modes of x/(u/v).

This trace is orthogonal to the stable strict-inference fault_mask, semantic_bottom_mask, and bottom_provenance attributes. Those runtime masks classify why a concrete sample bottomed; FRU structural provenance only records where symbolic denominator factors came from before runtime evaluation. When callers evaluate those structural validity factors through FlattenedFRU.structural_validity_failures(...), each factor fails closed on not finite(V_i) or |V_i| < tau_i; a non-finite factor value is never accepted just because its absolute value misses the threshold. FlattenedFRU.evaluate(...) applies the same factorwise check before accepting the reduced P/Q payload, so examples such as x/x -> (1, 1, {x}) still bottom at x = 0 under guarded strict FRU semantics. For a divided rational payload such as (a/b)/(u/v), guarded FRU flattening may emit the finite payload (a*v)/(b*u) only while retaining the erased v = 0 condition as a validity factor. Consumers that pass only the bare P/Q tensors to strict inference must evaluate those validity factors separately before accepting the decoded value.

Domain Assumptions¶

Pure Fracterm flattening may use Fracterm(...).flatten(domain_assumptions=[("x", "nonzero")]) to treat monomial denominator factors covered by caller-declared nonzero facts as safe for local simplifications such as x/x -> 1/1 or 0/x -> 0/1. Shared numeric constant factors may also be cancelled because nonzero constants cannot add a bottom location. Non-monomial denominator facts can be declared by passing the exact Polynomial object. These assumptions are contracts on the caller and are not runtime guards.

FRUExpression.flatten(..., domain_assumptions=[("x", "nonzero")]) records the assumption on FlattenedFRU.domain_assumptions for audit/export review. If simplification cancels a symbolic factor covered by a declared fact, FlattenedFRU.cancellation_domain_assumptions records the subset of assumptions tied to that cancellation. Those assumptions are caller contracts, not runtime guards. Evaluating FlattenedFRU.as_fracterm() or passing the bare P/Q tensors into strict inference does not check structural validity factors or verify that runtime inputs satisfy the declared nonzero facts. FlattenedFRU.evaluate(...) checks structural validity factors retained by the guarded artifact, but it does not validate caller-declared domain assumptions. If deployment data violates a declared nonzero assumption, that behavior is a caller-contract violation and is outside the flattened artifact's semantic guarantee unless the caller installs a separate validator before use.

Blow-up Limits and Refusal Criteria¶

The default FRU bound model uses d = max(d_p, d_q) for the incoming flattened head. After L fused rational layers, both the numerator and denominator are bounded by 2 ** (L - 1) * d. With the default max_depth=5, the largest accepted guarded-payload head is therefore capped at 16 * d for both P and Q.

Fused depth `L`	Max `deg(P)`	Max `deg(Q)`
1	`d`	`d`
2	`2 * d`	`2 * d`
3	`4 * d`	`4 * d`
4	`8 * d`	`8 * d`
5	`16 * d`	`16 * d`

The table above records the current guarded/field-rational payload degree budget: ordinary quotient division for (a/b)/(u/v) gives (a*v)/(b*u). Pure strict-preserving fracterm division can increase degree faster than field-rational division because (a/b)/(u/v) keeps the extra v^2 numerator factor and u*v denominator factor needed to preserve bottoms. For D(t) = max(deg(P_t), deg(Q_t)), a strict division node satisfies D(A / B) <= D(A) + 2D(B). When both operands are already at the same budget, the worst-case multiplier is 3. Balanced nested divisions can therefore grow like O(3^L d), not O(2^L d), giving this pure strict table:

Fused depth `L`	Pure strict max `deg(P)`	Pure strict max `deg(Q)`
1	`d`	`d`
2	`3 * d`	`3 * d`
3	`9 * d`	`9 * d`
4	`27 * d`	`27 * d`
5	`81 * d`	`81 * d`

A four-division chain after the seed, represented as fused depth L=5, therefore reaches 81 * d; at d=4, that is 324, compared with 64 under the current 16 * d guarded payload budget. Equivalently, counting only the four post-seed division layers as L=4, the pure strict worst-case calibration is 3^4 · 4 = 324, while a guarded finite-payload style bound near 2^4 · 4 = 64 is roughly a five-fold smaller finite-payload degree. The tradeoff is carrying up to four bounded-degree validity factors and checking them factorwise at runtime or audit time. Guarded strict FRU mode can avoid some of that blow-up by moving erased denominator conditions into validity factors instead of duplicating them in the finite payload; the reduced payload is strict-preserving only together with those factorwise checks.

FractermRationalUnit keeps the guarded payload budget by default and accepts degree_bound_model="pure_strict_division" when validating precomputed pure strict payloads that need the larger tripling budget. FractermRationalUnit.flatten_expression(...) checks the strict scm_strict artifact before honoring an explicit simplification_mode="field_rational" request; if strict flattening exceeds the configured depth or degree bounds, the call fails instead of using field-rational simplification as a rescue path. Callers that need a recorded audit outcome instead of an exception can pass preserve_unflattened=True. That opt-in still runs strict flattening and bound checks first; on a depth or degree refusal it returns UnflattenedFRUAudit, which stores the original typed expression and refusal metadata. The current preservation mode is explicitly audit_only: the record stores the original FRUExpression tree plus a flattening-refusal marker (refusal_kind and message) for audit/export review, does not evaluate at runtime, and exposes no eager fallback. It is not a pre-flatten shortcut and does not preserve artifacts that fail only after an explicit non-strict flattening mode. A future runtime fallback must be a separate opt-in, must evaluate the original tree with eager SCM semantics, and must be documented as slower than flattened P/Q evaluation.

Reference Head Budget Precheck¶

Before MR-flattening grows beyond the local FRU path, the current reference heads have the following head-local degree decisions. These budgets treat the learned backbone as a feature producer and only account for the symbolic rational head over those features. The canonical machine-readable copy lives in zeroproofml.layers.fru_degree_budgets.REFERENCE_FRU_DEGREE_BUDGETS.

Reference path	Head-local degrees	Depth / bounds	Decision
`examples/fru_strict_check_demo.py` sensor-gain × calibration × strict-guard demo	one flattened head, actual `P=3`, `Q=3`; retained conservative validity factor degree `1`	seed `d=1`, depth `4`; guarded bound `8`, pure strict bound `27`	Fits pure strict mode. The current guarded FRU artifact may retain the strict-guard source as audit metadata, but no `preserve_unflattened` path is needed.
RR IK benchmark projective rational heads (`zeroproof/layers/projective_rational.py`, `zeroproofml/benchmarks/domains/rr_scm.py`)	two scalar heads, `dtheta1` and `dtheta2`, each `P=3`, `Q=2` with a shared polynomial denominator feature	depth `1`; guarded and pure strict bounds both `3`	Fits pure strict mode.
RR IK reference deployment (`zeroproofml/reference_robotics_deployment.py`)	configured with P3/Q2 weights but `q_param="softplus"` and `q_min=1e-4`	outside the sparse-polynomial FRU fragment	Use `preserve_unflattened` for audit or restructure the denominator policy before MR-flattening.
DOSE projective SCM artifact path (`examples/dose/models.py`, `scripts/dose/run_dose_suite.py`)	one scalar `log_ic50` head, `P=3`, `Q=2`; auxiliary classifier and direction heads do not alter the strict P/Q payload	depth `1`; guarded and pure strict bounds both `3`	Fits pure strict mode.
DOSE angular SCM artifact path (`examples/dose/models.py`)	emits `P=cos(theta)`, `Q=sin(theta)`	outside the sparse-polynomial FRU fragment	Use `preserve_unflattened` for audit or restructure into a polynomial FRU head before MR-flattening.

This is only a degree bound, not a term-count bound: additions and divisions still cross-multiply sparse factors, so symbolic term counts can balloon well before a head becomes useful for audit or export. The hard depth cap is there to stop that symbolic blow-up from turning a local analysis pass into a whole-model expansion problem.

Flattening should be refused when:

the requested expression depth is above the configured FRU depth, or the FRU itself would exceed max_depth;
the flattened numerator or denominator degree exceeds the current bound, including the legacy coefficient-list flatten(...) path;
the graph contains nodes outside the typed algebraic fragment documented above, such as generic PyTorch control flow, unsupported nonlinearities, or whole-network lowering requests;
the caller is trying to symbolically expand a head inside the per-step training loop instead of using the projective/tuple carrier;
the plan relies on a later simplification pass to rescue an already out-of-bounds expression. Simplification is optional cleanup, not a license to skip the safety bounds.

Worked Example¶

Consider a two-layer FRU ((x + 1) / x) / (x - 1). Flattening produces

P(x) = x + 1
Q(x) = x(x - 1)

so the singularities live at x ∈ {0, 1} and can be detected by checking Q(x) once, instead of monitoring every intermediate op.

For a runnable end-to-end example, see examples/fru_strict_check_demo.py. That script composes a sensor_gain stage, a calibration stage, and a final strict_guard, flattens the whole head with FractermRationalUnit.flatten_expression(...), and then feeds the resulting P/Q tensors into strict_inference(...) so the final denominator is checked once per sample.

Placement Decision¶

During training: no. Training already has a smoother carrier in the projective/tuple path, so rebuilding symbolic P/Q polynomials every step adds expansion cost without changing the optimization objective.
As a post-training analysis pass: yes, this is the preferred default. Once the head structure is fixed, flattening gives a stable artifact for degree-bound checks, denominator-provenance review, and equivalence tests against the composed expression.
Only at export time: no. Export should be able to reuse or revalidate an already-audited flattened artifact, but waiting until packaging hides bound violations and denominator-growth surprises until the last stage.

The project decision is therefore: keep training in projective form, run flattening explicitly as a post-training analysis pass, and optionally repeat or validate that same flattening at export when a bundle needs an explicit P/Q artifact.

Authoring Guidelines¶

Represent rational heads explicitly as (numerator, denominator) pairs or helper classes so the final denominator is easy to inspect.
Prefer shallow FRUs (depth ≤ 5) to keep polynomial degrees manageable; at the default guarded cap the degree multiplier is already 16 * d, while pure strict division can require 81 * d.
Document where flattening occurs in layer docstrings so Sphinx/MkDocs can surface the singularity story alongside the API.

References¶

J.A. Bergstra and A. Ponse, Common Meadows (2019 revision)
J.A. Bergstra and J.V. Tucker, Fracterm calculus and totalised fields