Advanced nonlinear and correlation-aware error propagation #297

Context

Follow-up to #172. The core issue introduces typed result guarantees, conservative basic propagation, budget allocation, and fail-closed legality for approximate-over-approximate plans.

Many useful operators do not have a finite global L1/Lipschitz bound, or produce unusably loose bounds when propagated with independent scalar intervals. This issue adds domain-aware nonlinear and correlation-aware propagation without weakening #172's safety rule: no sound rule means the candidate remains illegal.

Scope

General norm conversion

Support typed induced-operator bounds:

||f(x_hat) - f(x)||_q
    <= L_(p->q) * ||x_hat - x||_p

Represent L1, L2, LInf, and explicitly supported Lp norms. Norm conversion requires dimension/cardinality evidence and must not happen implicitly.

Domain-aware local bounds

Carry a proven value domain alongside an error guarantee:

struct ResultGuarantee {
    error: ErrorBound,
    value_domain: Option<ValueRegion>,
    assumptions: AssumptionSet,
    // probability and provenance omitted here
}

Operators may derive a local bound only when their domain preconditions are proved. For example, reciprocal/division requires a denominator interval that excludes zero.

Interval extension

Implement monotone and interval-arithmetic rules for selected scalar operators:

x in [lx, ux] -> exp(x) in [exp(lx), exp(ux)]
x in [lx, ux], lx > 0 -> log(x) in [log(lx), log(ux)]

Division by an interval containing zero returns UnboundedComposition.

Jacobian and Taylor remainder

For supported differentiable multi-input operators, permit a certified local rule:

||delta_y||_q
    <= sup_domain ||J_f(x)||_(p->q) * ||delta_x||_p

Where first-order propagation is insufficient, represent a bounded remainder:

f(x + delta_x)
    = f(x) + J_f(x) delta_x + R_2

|R_2| <= 1/2 * sup_domain ||H_f|| * ||delta_x||^2

Do not implement an unrestricted symbolic calculus engine initially; register explicit rules for concrete operators.

Correlation-aware affine errors

Preserve shared error-source identity so reuse of one approximate value does not get treated as independent errors:

struct ErrorTerm {
    source_id: ErrorSourceId,
    coefficient: BoundExpr,
}

ErrorBound::Affine {
    center: BoundExpr,
    terms: Vec<ErrorTerm>,
    remainder: BoundExpr,
}

For example, x_hat - x_hat from the same error source should cancel rather than produce twice the interval radius.

Architectural requirements

• Extend Propagate end-to-end accuracy guarantees for approximate-over-approximate plans #172's AccuracyModel; do not add propagation decisions to CostModel.
• Every conditional bound records its domain assumptions and provenance.
• Candidate legality requires all assumptions to be proved from schema/statistics/runtime capability.
• Missing dimensions, domains, derivatives, or correlation evidence produce a typed unsupported/unbounded result.
• Posterior/empirical evidence must remain distinguishable from deterministic or probabilistic a priori guarantees.

Acceptance criteria

• L2 and LInf examples use the correct induced operator norm.
• Reciprocal/division is accepted when the denominator domain excludes zero and rejected otherwise.
• At least one nonlinear operator uses a certified Jacobian or Taylor-remainder rule.
• Shared-source affine terms cancel in x - x; independent source IDs do not.
• Interval and affine guarantees serialize with assumptions and provenance and appear explicitly in DAG export.
• Unsupported nonlinear composition remains KeepPreAsap/raw fallback rather than silently treating an input as exact.
• Tests cover bound soundness against enumerated finite-domain inputs for each initially registered rule.

Non-goals

• Assuming global Lipschitz continuity when only a local bound exists.
• Inferring statistical independence from distinct DAG nodes.
• Treating benchmark-only empirical error as a strict AccuracyTarget proof.
• Protocol-specific fallback execution.