omnibias.core.verified.jet_flow
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.verified.jet_flowModule contract & mathematical conventions
Exact-Jacobian + high-order jet Lohner steps (theory 07-06).
Validated integration is limited by wrapping and by the Jacobian
enclosure. For fields in the activation dictionary the founding
bias collapse (delta -> 0) supplies Df and the solution
Taylor coefficients from one sigma evaluation per order.
Temperature collapse (beta -> inf, feasibility) does not
appear. Do not conflate the two.
Every run emits a WidthBudget. The existing
~omnibias.core.verified.lohner.lohner_flow path is
untouched (G6). Scope is one field, one initial box, one
finite horizon. This is not a continuum existence theorem,
not an attractor statement or a global
regularity result.
Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.
DISCLAIMER
omnibias.core.verified.jet_flow.DISCLAIMERSource ↗DISCLAIMER = 'finite-horizon enclosure of one trajectory from one initial box; with bounds local to the specified horizon and box'This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.
Regression example · seal refuses forged kernel flag
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_seal_refuses_forged_kernel_flag() -> None:
with pytest.raises(ValueError):
make_certificate(
claim="finite-horizon Lohner enclosure of one trajectory",
payload={"disclaimer": DISCLAIMER},
honesty={"theorem_prover_verified": True},
)python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_seal_refuses_forged_kernel_flag -qRegression example · g1 width budget on every run
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g1_width_budget_on_every_run -qRead the implementation
DISCLAIMER = (
"finite-horizon enclosure of one trajectory from one initial box; "
"with bounds local to the specified horizon and box"
)OrbitProof
omnibias.core.verified.jet_flow.OrbitProofSource ↗class OrbitProofDataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.
Krawczyk periodic-point certificate of a time-period map.
Parameters
| Name | Type & default | Contract |
|---|---|---|
existsdataclass field | boolRequired | See the operation contract and implementation below. |
perioddataclass field | floatRequired | See the operation contract and implementation below. |
centerdataclass field | tuple[float, ...]Required | See the operation contract and implementation below. |
enclosuredataclass field | tuple[tuple[float, float], ...] | NoneRequired | See the operation contract and implementation below. |
kappadataclass field | float | NoneRequired | See the operation contract and implementation below. |
budgetdataclass field | WidthBudget | NoneRequired | See the operation contract and implementation below. |
Fields & methods
existsfield
exists: boolDeclared bool field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗periodfield
period: floatDeclared float field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗centerfield
center: tuple[float, ...]Declared tuple[float, ...] field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗enclosurefield
enclosure: tuple[tuple[float, float], ...] | NoneDeclared tuple[tuple[float, float], ...] | None field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗kappafield
kappa: float | NoneDeclared float | None field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗budgetfield
budget: WidthBudget | NoneDeclared WidthBudget | None field on OrbitProof. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗Read the implementation
class OrbitProof:
"""Krawczyk periodic-point certificate of a time-``period`` map."""
exists: bool
period: float
center: tuple[float, ...]
enclosure: tuple[tuple[float, float], ...] | None
kappa: float | None
budget: WidthBudget | NoneSCHEMA_VERSION
omnibias.core.verified.jet_flow.SCHEMA_VERSIONSource ↗SCHEMA_VERSION = 'validated-dynamics-jet-flow-1'This exported constant is defined by the expression above. Its exact value and annotation come from the pinned source; use it with the module contract.
Read the implementation
SCHEMA_VERSION = "validated-dynamics-jet-flow-1"TowerFieldSpec
omnibias.core.verified.jet_flow.TowerFieldSpecSource ↗class TowerFieldSpecDataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.
Activation-dictionary field consumed by tower_jacobian.
Parameters
| Name | Type & default | Contract |
|---|---|---|
namedataclass field | strRequired | See the operation contract and implementation below. |
scaledataclass field | floatDefault: 1.0 | See the operation contract and implementation below. |
biasdataclass field | floatDefault: 0.0 | See the operation contract and implementation below. |
kinddataclass field | strDefault: 'scalar' | See the operation contract and implementation below. |
stiffnessdataclass field | floatDefault: 1.0 | See the operation contract and implementation below. |
dampingdataclass field | floatDefault: 0.0 | See the operation contract and implementation below. |
Executed regression · coefficient arithmetic chooses interval
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_coefficient_arithmetic_chooses_interval() -> None:
report = coefficient_arithmetic_report()
assert report["choice"] == "interval"
assert report["tm_required"] is Falsepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -qFields & methods
namefield
name: strDeclared str field on TowerFieldSpec. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗scalefield
scale: float = 1.0Declared float field on TowerFieldSpec. Default expression: 1.0.
biasfield
bias: float = 0.0Declared float field on TowerFieldSpec. Default expression: 0.0.
kindfield
kind: str = 'scalar'Declared str field on TowerFieldSpec. Default expression: 'scalar'.
stiffnessfield
stiffness: float = 1.0Declared float field on TowerFieldSpec. Default expression: 1.0.
dampingfield
damping: float = 0.0Declared float field on TowerFieldSpec. Default expression: 0.0.
__post_init__method
__post_init__(self) -> NoneSee the class contract above and the exact method implementation below.
Returns: None
Validation & failure cases
- When
kind not in {'scalar', 'oscillator'}, raisesValueError(f'kind must be scalar or oscillator, got {self.kind!r}').
Executed regression · coefficient arithmetic chooses interval
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_coefficient_arithmetic_chooses_interval() -> None:
report = coefficient_arithmetic_report()
assert report["choice"] == "interval"
assert report["tm_required"] is Falsepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -qMethod implementation
def __post_init__(self) -> None:
kind = str(self.kind).lower().strip()
if kind not in {"scalar", "oscillator"}:
raise ValueError(f"kind must be scalar or oscillator, got {self.kind!r}")
object.__setattr__(self, "kind", kind)
object.__setattr__(self, "name", str(self.name).lower().strip())Read the implementation
class TowerFieldSpec:
"""Activation-dictionary field consumed by :func:`tower_jacobian`."""
name: str
scale: float = 1.0
bias: float = 0.0
kind: str = "scalar"
stiffness: float = 1.0
damping: float = 0.0
def __post_init__(self) -> None:
kind = str(self.kind).lower().strip()
if kind not in {"scalar", "oscillator"}:
raise ValueError(f"kind must be scalar or oscillator, got {self.kind!r}")
object.__setattr__(self, "kind", kind)
object.__setattr__(self, "name", str(self.name).lower().strip())ValidatedRun
omnibias.core.verified.jet_flow.ValidatedRunSource ↗class ValidatedRunDataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.
One finite-horizon Lohner integration plus its width budget.
Parameters
| Name | Type & default | Contract |
|---|---|---|
statedataclass field | LohnerSetRequired | See the operation contract and implementation below. |
budgetdataclass field | WidthBudgetRequired | See the operation contract and implementation below. |
horizondataclass field | floatRequired | See the operation contract and implementation below. |
n_stepsdataclass field | intRequired | See the operation contract and implementation below. |
orderdataclass field | intRequired | See the operation contract and implementation below. |
Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qFields & methods
statefield
state: LohnerSetDeclared LohnerSet field on ValidatedRun. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗budgetfield
budget: WidthBudgetDeclared WidthBudget field on ValidatedRun. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗horizonfield
horizon: floatDeclared float field on ValidatedRun. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗n_stepsfield
n_steps: intDeclared int field on ValidatedRun. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗orderfield
order: intDeclared int field on ValidatedRun. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗widthproperty
width(self) -> floatSee the class contract above and the exact method implementation below.
Returns: float
Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qMethod implementation
def width(self) -> float:
return float(self.state.width())Read the implementation
class ValidatedRun:
"""One finite-horizon Lohner integration plus its width budget."""
state: LohnerSet
budget: WidthBudget
horizon: float
n_steps: int
order: int
@property
def width(self) -> float:
return float(self.state.width())WidthBudget
omnibias.core.verified.enclosure_collapse.WidthBudgetSource ↗class WidthBudgetDataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.
Per-run width split. Required before any improvement claim.
Parameters
| Name | Type & default | Contract |
|---|---|---|
truncationdataclass field | floatRequired | See the operation contract and implementation below. |
jacobiandataclass field | floatRequired | See the operation contract and implementation below. |
wrappingdataclass field | floatRequired | See the operation contract and implementation below. |
roundingdataclass field | floatRequired | See the operation contract and implementation below. |
Executed regression · diagnose width maps each dominant
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_diagnose_width_maps_each_dominant() -> None:
expected = {
"truncation": "raise_order",
"wrapping": "subdivide",
"jacobian": "shrink_step",
"rounding": "stop_floor",
}
for dominant, action in expected.items():
parts = {"truncation": 0.0, "jacobian": 0.0, "wrapping": 0.0, "rounding": 0.0}
parts[dominant] = 1.0
rec = diagnose_width(WidthBudget(**parts))
assert isinstance(rec, RecommendedAction)
assert rec.dominant == dominant
assert rec.action == action
payload = rec.to_payload()
assert payload["dominant"] == dominant
assert payload["action"] == action
assert payload["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_enclosure_collapse.py::test_diagnose_width_maps_each_dominant" -qRegression example · g6 lohner flow bit unchanged
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g6_lohner_flow_bit_unchanged() -> None:
snap_a = lohner_regression_snapshot()
snap_b = lohner_regression_snapshot()
assert snap_a == snap_b
a = [[0.0, -1.0], [1.0, 0.0]]
field = linear_field(a)
jac = constant_jacobian(a)
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
# The jet wrapper must reproduce the same step as lohner_step.
state = LohnerSet.from_box(y0)
jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
plain = lohner_step(field, jac, state, 0.05, 12)
for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
assert left.lo == right.lo and left.hi == right.hi
assert isinstance(budget, WidthBudget)
wrap = naive_vs_lohner_wrapping()
assert wrap["naive"] > wrap["lohner"]
# Existing path still encloses the rotation centre.
box = classic.to_box()
assert box[0].lo <= math.cos(1.0) <= box[0].hipython -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g6_lohner_flow_bit_unchanged -qFields & methods
truncationfield
truncation: floatDeclared float field on WidthBudget. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗jacobianfield
jacobian: floatDeclared float field on WidthBudget. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗wrappingfield
wrapping: floatDeclared float field on WidthBudget. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗roundingfield
rounding: floatDeclared float field on WidthBudget. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗totalproperty
total(self) -> floatSee the class contract above and the exact method implementation below.
Returns: float
Executed regression · g1 width budget on every run
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g1_width_budget_on_every_run" -qMethod implementation
def total(self) -> float:
return float(
self.truncation + self.jacobian + self.wrapping + self.rounding
)dominantproperty
dominant(self) -> strSee the class contract above and the exact method implementation below.
Returns: str
Executed regression · diagnose width maps each dominant
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_diagnose_width_maps_each_dominant() -> None:
expected = {
"truncation": "raise_order",
"wrapping": "subdivide",
"jacobian": "shrink_step",
"rounding": "stop_floor",
}
for dominant, action in expected.items():
parts = {"truncation": 0.0, "jacobian": 0.0, "wrapping": 0.0, "rounding": 0.0}
parts[dominant] = 1.0
rec = diagnose_width(WidthBudget(**parts))
assert isinstance(rec, RecommendedAction)
assert rec.dominant == dominant
assert rec.action == action
payload = rec.to_payload()
assert payload["dominant"] == dominant
assert payload["action"] == action
assert payload["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_enclosure_collapse.py::test_diagnose_width_maps_each_dominant" -qMethod implementation
def dominant(self) -> str:
parts = {
"truncation": self.truncation,
"jacobian": self.jacobian,
"wrapping": self.wrapping,
"rounding": self.rounding,
}
return max(parts, key=lambda key: parts[key])to_payloadmethod
to_payload(self) -> dict[str, object]See the class contract above and the exact method implementation below.
Returns: dict[str, object]
Executed regression · g1 width budget on every run
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g1_width_budget_on_every_run" -qMethod implementation
def to_payload(self) -> dict[str, object]:
return {
"truncation": self.truncation,
"jacobian": self.jacobian,
"wrapping": self.wrapping,
"rounding": self.rounding,
"dominant": self.dominant,
"total": self.total,
}Read the implementation
class WidthBudget:
"""Per-run width split. Required before any improvement claim."""
truncation: float
jacobian: float
wrapping: float
rounding: float
@property
def total(self) -> float:
return float(
self.truncation + self.jacobian + self.wrapping + self.rounding
)
@property
def dominant(self) -> str:
parts = {
"truncation": self.truncation,
"jacobian": self.jacobian,
"wrapping": self.wrapping,
"rounding": self.rounding,
}
return max(parts, key=lambda key: parts[key])
def to_payload(self) -> dict[str, object]:
return {
"truncation": self.truncation,
"jacobian": self.jacobian,
"wrapping": self.wrapping,
"rounding": self.rounding,
"dominant": self.dominant,
"total": self.total,
}Other public import paths
omnibias.core.verified.enclosure_collapse.WidthBudgetomnibias.core.verified.jet_flow.WidthBudget
adaptive_step_from_singularity
omnibias.core.verified.jet_flow.adaptive_step_from_singularitySource ↗adaptive_step_from_singularity(field: VectorField, state: LohnerSet, *, order: int, safety: float=0.5, max_step: float=1.0) -> floatSuggest a step below the jet radius of convergence (then validate).
The radius is a coefficient estimate, not a proof. The returned
step is a suggestion; lohner_step_jet still has to accept
the a-priori enclosure.
Parameters
| Name | Type & default | Contract |
|---|---|---|
fieldpositional-or-keyword | VectorFieldRequired | See the operation contract and implementation below. |
statepositional-or-keyword | LohnerSetRequired | See the operation contract and implementation below. |
orderkeyword-only | intRequired | See the operation contract and implementation below. |
safetykeyword-only | floatDefault: 0.5 | See the operation contract and implementation below. |
max_stepkeyword-only | floatDefault: 1.0 | See the operation contract and implementation below. |
floatExplicit validation & failure cases
- When
order < 2, raisesValueError(f'order must be >= 2, got {order}'). - When
not 0.0 < safety <= 1.0, raisesValueError(f'safety must be in (0, 1], got {safety}'). - When
max_step <= 0.0, raisesValueError(f'max_step must be positive, got {max_step}').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g5 singularity step soundness
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g5_singularity_step_soundness() -> None:
rows = singularity_step_report()
assert len(rows) == 3
assert all(row["sound"] for row in rows), rows
riccati = next(row for row in rows if row["name"] == "riccati")
assert riccati["step"] <= 1.0
tan_row = next(row for row in rows if row["name"] == "tan")
assert tan_row["step"] <= 0.5 * math.pipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g5_singularity_step_soundness" -qRead the implementation
def adaptive_step_from_singularity(
field: VectorField,
state: LohnerSet,
*,
order: int,
safety: float = 0.5,
max_step: float = 1.0,
) -> float:
"""Suggest a step below the jet radius of convergence (then validate).
The radius is a coefficient estimate, not a proof. The returned
step is a suggestion; :func:`lohner_step_jet` still has to accept
the a-priori enclosure.
"""
if order < 2:
raise ValueError(f"order must be >= 2, got {order}")
if not 0.0 < safety <= 1.0:
raise ValueError(f"safety must be in (0, 1], got {safety}")
if max_step <= 0.0:
raise ValueError(f"max_step must be positive, got {max_step}")
point = [Interval.point(c.mid) for c in state.center]
coeffs = _solution_coeffs(field, point, order)
radius = min(_series_radius([c.mid for c in row]) for row in coeffs)
if math.isinf(radius):
return float(max_step)
step = safety * radius
if not math.isfinite(step) or step <= 0.0:
return min(float(max_step), 1e-3)
return min(float(max_step), step)clock_field
omnibias.core.verified.jet_flow.clock_fieldSource ↗clock_field() -> tuple[VectorField, JacobianEnclosure]x' = 1. Entire, Jacobian zero.
tuple[VectorField, JacobianEnclosure]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def clock_field() -> tuple[VectorField, JacobianEnclosure]:
"""``x' = 1``. Entire, Jacobian zero."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
return [TaylorSeries.constant(1.0, series[0].order)]
def jac(_box: Sequence[Interval]) -> IntervalMatrix:
return [[Interval.point(0.0)]]
return field, jaccoefficient_arithmetic_report
omnibias.core.verified.jet_flow.coefficient_arithmetic_reportSource ↗coefficient_arithmetic_report() -> dict[str, Any]Interval Taylor vs a point jet: TM is not required when G3 holds.
dict[str, Any]Executed regression · coefficient arithmetic chooses interval
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_coefficient_arithmetic_chooses_interval() -> None:
report = coefficient_arithmetic_report()
assert report["choice"] == "interval"
assert report["tm_required"] is Falsepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -qRegression example · g2 jacobian containment
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g2_jacobian_containment -qRead the implementation
def coefficient_arithmetic_report() -> dict[str, Any]:
"""Interval Taylor vs a point jet: TM is not required when G3 holds."""
spec = TowerFieldSpec("tanh")
field = tower_field(spec)
point = [Interval.point(0.3)]
box = [Interval(0.2, 0.4)]
order = 12
p_coeffs = _solution_coeffs(field, point, order + 1)
b_coeffs = _solution_coeffs(field, box, order + 1)
p_w = p_coeffs[0][order + 1].width
b_w = b_coeffs[0][order + 1].width
ratio = b_w / p_w if p_w > 0.0 else 0.0
return {
"choice": "interval",
"box_over_point": ratio,
"tm_required": False,
"justification": (
"interval Taylor coefficients on the 07-06 suite keep the "
"order-12 remainder finite; Taylor models are not required "
"to pass G3"
),
}cubic_oscillator
omnibias.core.verified.jet_flow.cubic_oscillatorSource ↗cubic_oscillator() -> tuple[VectorField, JacobianEnclosure]Polynomial oscillator y' = z, z' = -y^3.
tuple[VectorField, JacobianEnclosure]Read the implementation
def cubic_oscillator() -> tuple[VectorField, JacobianEnclosure]:
"""Polynomial oscillator ``y' = z``, ``z' = -y^3``."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
y, z = series[0], series[1]
return [z, -(y * y * y)]
def jac(box: Sequence[Interval]) -> IntervalMatrix:
y = box[0]
return [
[Interval.point(0.0), Interval.point(1.0)],
[Interval.point(-3.0) * y * y, Interval.point(0.0)],
]
return field, jacdecay_field
omnibias.core.verified.jet_flow.decay_fieldSource ↗decay_field(rate: float=0.25) -> tuple[VectorField, JacobianEnclosure]Linear decay x' = -rate x.
Parameters
| Name | Type & default | Contract |
|---|---|---|
ratepositional-or-keyword | floatDefault: 0.25 | See the operation contract and implementation below. |
tuple[VectorField, JacobianEnclosure]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def decay_field(rate: float = 0.25) -> tuple[VectorField, JacobianEnclosure]:
"""Linear decay ``x' = -rate x``."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
return [series[0] * (-rate)]
def jac(_box: Sequence[Interval]) -> IntervalMatrix:
return [[Interval.point(-rate)]]
return field, jacexp_field
omnibias.core.verified.jet_flow.exp_fieldSource ↗exp_field() -> VectorFieldx' = x. Entire solution; radius is infinite.
VectorFieldExecuted regression · g5 singularity step soundness
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g5_singularity_step_soundness() -> None:
rows = singularity_step_report()
assert len(rows) == 3
assert all(row["sound"] for row in rows), rows
riccati = next(row for row in rows if row["name"] == "riccati")
assert riccati["step"] <= 1.0
tan_row = next(row for row in rows if row["name"] == "tan")
assert tan_row["step"] <= 0.5 * math.pipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g5_singularity_step_soundness" -qRead the implementation
def exp_field() -> VectorField:
"""``x' = x``. Entire solution; radius is infinite."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
return [series[0]]
return fieldfrozen_field
omnibias.core.verified.jet_flow.frozen_fieldSource ↗frozen_field() -> tuple[VectorField, JacobianEnclosure]x' = 0. The set is invariant.
tuple[VectorField, JacobianEnclosure]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def frozen_field() -> tuple[VectorField, JacobianEnclosure]:
"""``x' = 0``. The set is invariant."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
return [TaylorSeries.constant(0.0, series[0].order)]
def jac(_box: Sequence[Interval]) -> IntervalMatrix:
return [[Interval.point(0.0)]]
return field, jachonesty_payload
omnibias.core.verified.jet_flow.honesty_payloadSource ↗honesty_payload() -> dict[str, bool]Honesty flags. theorem_prover_verified is reported False, never sealed.
dict[str, bool]Executed regression · g1 width budget on every run
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g1_width_budget_on_every_run" -qRead the implementation
def honesty_payload() -> dict[str, bool]:
"""Honesty flags. ``theorem_prover_verified`` is reported False, never sealed."""
return {
"unproven_claim": False,
"continuum_existence_claim": False,
"attractor_claim": False,
"theorem_prover_verified": False,
}hopf_cartesian
omnibias.core.verified.jet_flow.hopf_cartesianSource ↗hopf_cartesian(mu: float=1.0) -> tuple[VectorField, JacobianEnclosure]2-D Hopf normal form. Unreduced time-T points are non-isolated.
Parameters
| Name | Type & default | Contract |
|---|---|---|
mupositional-or-keyword | floatDefault: 1.0 | See the operation contract and implementation below. |
tuple[VectorField, JacobianEnclosure]Read the implementation
def hopf_cartesian(mu: float = 1.0) -> tuple[VectorField, JacobianEnclosure]:
"""2-D Hopf normal form. Unreduced time-``T`` points are non-isolated."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
x, y = series[0], series[1]
r2 = x * x + y * y
return [x * mu - y - x * r2, x + y * mu - y * r2]
def jac(box: Sequence[Interval]) -> IntervalMatrix:
x, y = box[0], box[1]
m = Interval.point(mu)
three = Interval.point(3.0)
two = Interval.point(2.0)
x2, y2 = x.pow_int(2), y.pow_int(2)
return [
[m - (three * x2 + y2), Interval.point(-1.0) - two * x * y],
[Interval.point(1.0) - two * x * y, m - (x2 + three * y2)],
]
return field, jachorizon_report
omnibias.core.verified.jet_flow.horizon_reportSource ↗horizon_report() -> list[dict[str, Any]]G3: at 5x the baseline time the jet width still sits under the baseline cap.
list[dict[str, Any]]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def horizon_report() -> list[dict[str, Any]]:
"""G3: at 5x the baseline time the jet width still sits under the baseline cap."""
rows: list[dict[str, Any]] = []
h_base = 0.05
steps_base = 16
order_base = 4
order_jet = 12
t_base = h_base * steps_base
for name, field, jac, y0 in horizon_suite():
base = lohner_flow(field, jac, y0, h_base, steps_base, order=order_base)
cap = max(base.width(), 1e-14)
h_jet = min(0.40, _largest_step(field, jac, y0, order_jet, h_hi=0.8))
t_target = 5.0 * t_base
n_jet = max(1, int(math.ceil(t_target / h_jet)))
try:
jet = lohner_flow_jet(field, jac, y0, h_jet, n_jet, order=order_jet)
t_jet = jet.horizon
width_jet = jet.width
ok = width_jet <= cap * 1.05 + 1e-15 and t_jet + 1e-12 >= t_target
except (ValueError, RuntimeError, OverflowError, ZeroDivisionError):
t_jet = 0.0
width_jet = math.inf
ok = False
ratio = t_jet / t_base if t_base > 0.0 else 0.0
rows.append(
{
"name": name,
"t_base": t_base,
"t_jet": t_jet,
"ratio": ratio,
"cap": cap,
"width_jet": width_jet,
"h_jet": h_jet,
"win": ok and ratio >= 5.0,
}
)
return rowshorizon_suite
omnibias.core.verified.jet_flow.horizon_suiteSource ↗horizon_suite() -> list[tuple[str, VectorField, JacobianEnclosure, list[Interval]]]Ten isometries / contractions so wrapping, not true expansion, binds.
list[tuple[str, VectorField, JacobianEnclosure, list[Interval]]]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def horizon_suite() -> list[tuple[str, VectorField, JacobianEnclosure, list[Interval]]]:
"""Ten isometries / contractions so wrapping, not true expansion, binds."""
rot = [[0.0, -1.0], [1.0, 0.0]]
slow = [[0.0, -0.5], [0.5, 0.0]]
spiral = [[-0.2, -1.0], [1.0, -0.2]]
spiral2 = [[-0.4, -0.7], [0.7, -0.4]]
rad_f, rad_j = radial_hopf(1.0)
decay_f, decay_j = decay_field(0.25)
mid_d, mid_j = decay_field(0.5)
fast_d, fast_j = decay_field(1.0)
clock_f, clock_j = clock_field()
frozen_f, frozen_j = frozen_field()
thin = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
return [
("rotation", linear_field(rot), constant_jacobian(rot), thin),
("slow_rotation", linear_field(slow), constant_jacobian(slow),
[Interval(0.7, 0.71), Interval(-0.01, 0.01)]),
("contracting_spiral", linear_field(spiral), constant_jacobian(spiral), thin),
("contracting_spiral2", linear_field(spiral2), constant_jacobian(spiral2), thin),
("radial_hopf", rad_f, rad_j, [Interval(0.999, 1.001)]),
("decay", decay_f, decay_j, [Interval(0.4, 0.5)]),
("mid_decay", mid_d, mid_j, [Interval(0.4, 0.5)]),
("fast_decay", fast_d, fast_j, [Interval(0.4, 0.5)]),
("clock", clock_f, clock_j, [Interval(-0.1, 0.1)]),
("frozen", frozen_f, frozen_j, [Interval(-0.2, 0.2)]),
]jacobian_containment_report
omnibias.core.verified.jet_flow.jacobian_containment_reportSource ↗jacobian_containment_report(*, n_boxes: int=1000, seed: int=0) -> dict[str, Any]G2: enclosure contains the true Jacobian on n_boxes per field.
Parameters
| Name | Type & default | Contract |
|---|---|---|
n_boxeskeyword-only | intDefault: 1000 | See the operation contract and implementation below. |
seedkeyword-only | intDefault: 0 | See the operation contract and implementation below. |
dict[str, Any]Executed regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRead the implementation
def jacobian_containment_report(
*,
n_boxes: int = 1000,
seed: int = 0,
) -> dict[str, Any]:
"""G2: enclosure contains the true Jacobian on ``n_boxes`` per field."""
import random
rng = random.Random(seed)
fields = named_tower_fields()
misses = 0
checked = 0
per_field: list[dict[str, Any]] = []
for spec in fields:
jac = tower_jacobian(spec)
dim = 1 if spec.kind == "scalar" else 2
field_misses = 0
for _ in range(n_boxes):
half = [0.01 + 0.19 * rng.random() for _ in range(dim)]
mid = [rng.uniform(-2.0, 2.0) for _ in range(dim)]
box = [Interval(mid[i] - half[i], mid[i] + half[i]) for i in range(dim)]
point = [mid[i] + (2.0 * rng.random() - 1.0) * half[i] * 0.9 for i in range(dim)]
enclosed = jac(box)
truth = _true_jacobian_at(spec, point)
ok = True
for i in range(len(truth)):
for j in range(len(truth[i])):
if not (enclosed[i][j].lo <= truth[i][j] <= enclosed[i][j].hi):
ok = False
checked += 1
if not ok:
misses += 1
field_misses += 1
per_field.append(
{"name": f"{spec.kind}:{spec.name}", "misses": field_misses, "n": n_boxes}
)
return {
"fields": len(fields),
"boxes_per_field": n_boxes,
"checked": checked,
"misses": misses,
"containment": misses == 0,
"per_field": per_field,
}lohner_flow_jet
omnibias.core.verified.jet_flow.lohner_flow_jetSource ↗lohner_flow_jet(field: VectorField, jac: JacobianEnclosure, y0: Sequence[IntervalLike], h: float, n_steps: int, order: int=12) -> ValidatedRunIntegrate with lohner_step_jet and accumulate a width budget.
Parameters
| Name | Type & default | Contract |
|---|---|---|
fieldpositional-or-keyword | VectorFieldRequired | See the operation contract and implementation below. |
jacpositional-or-keyword | JacobianEnclosureRequired | See the operation contract and implementation below. |
y0positional-or-keyword | Sequence[IntervalLike]Required | See the operation contract and implementation below. |
hpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
n_stepspositional-or-keyword | intRequired | See the operation contract and implementation below. |
orderpositional-or-keyword | intDefault: 12 | See the operation contract and implementation below. |
ValidatedRunExplicit validation & failure cases
- When
n_steps < 1, raisesValueError('n_steps must be >= 1').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRegression example · g1 width budget on every run
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g1_width_budget_on_every_run -qRead the implementation
def lohner_flow_jet(
field: VectorField,
jac: JacobianEnclosure,
y0: Sequence[IntervalLike],
h: float,
n_steps: int,
order: int = 12,
) -> ValidatedRun:
"""Integrate with :func:`lohner_step_jet` and accumulate a width budget."""
if n_steps < 1:
raise ValueError("n_steps must be >= 1")
state = LohnerSet.from_box(y0)
budget = _zero_budget()
for _ in range(n_steps):
state, piece = lohner_step_jet(state, field, jac, order=order, h=h)
budget = _merge_budget(budget, piece)
return ValidatedRun(state, budget, h * n_steps, n_steps, order)lohner_regression_snapshot
omnibias.core.verified.jet_flow.lohner_regression_snapshotSource ↗lohner_regression_snapshot() -> dict[str, float]Frozen lohner_flow numbers. The jet path must not change these.
dict[str, float]Executed regression · g6 lohner flow bit unchanged
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g6_lohner_flow_bit_unchanged() -> None:
snap_a = lohner_regression_snapshot()
snap_b = lohner_regression_snapshot()
assert snap_a == snap_b
a = [[0.0, -1.0], [1.0, 0.0]]
field = linear_field(a)
jac = constant_jacobian(a)
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
# The jet wrapper must reproduce the same step as lohner_step.
state = LohnerSet.from_box(y0)
jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
plain = lohner_step(field, jac, state, 0.05, 12)
for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
assert left.lo == right.lo and left.hi == right.hi
assert isinstance(budget, WidthBudget)
wrap = naive_vs_lohner_wrapping()
assert wrap["naive"] > wrap["lohner"]
# Existing path still encloses the rotation centre.
box = classic.to_box()
assert box[0].lo <= math.cos(1.0) <= box[0].hipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g6_lohner_flow_bit_unchanged" -qRead the implementation
def lohner_regression_snapshot() -> dict[str, float]:
"""Frozen ``lohner_flow`` numbers. The jet path must not change these."""
a = [[0.0, -1.0], [1.0, 0.0]]
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
final = lohner_flow(linear_field(a), constant_jacobian(a), y0, 0.05, 20, order=12)
box = final.to_box()
return {
"width": final.width(),
"x_lo": box[0].lo,
"x_hi": box[0].hi,
"y_lo": box[1].lo,
"y_hi": box[1].hi,
}lohner_step_jet
omnibias.core.verified.jet_flow.lohner_step_jetSource ↗lohner_step_jet(state: LohnerSet, field: VectorField, jac: JacobianEnclosure, *, order: int, h: float) -> tuple[LohnerSet, WidthBudget]Order-p QR-Lohner step. Same update as lohner_step.
Parameters
| Name | Type & default | Contract |
|---|---|---|
statepositional-or-keyword | LohnerSetRequired | See the operation contract and implementation below. |
fieldpositional-or-keyword | VectorFieldRequired | See the operation contract and implementation below. |
jacpositional-or-keyword | JacobianEnclosureRequired | See the operation contract and implementation below. |
orderkeyword-only | intRequired | See the operation contract and implementation below. |
hkeyword-only | floatRequired | See the operation contract and implementation below. |
tuple[LohnerSet, WidthBudget]Explicit validation & failure cases
- When
order < 1, raisesValueError(f'order must be >= 1, got {order}'). - When
h <= 0.0, raisesValueError(f'h must be positive, got {h}').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRegression example · g6 lohner flow bit unchanged
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g6_lohner_flow_bit_unchanged() -> None:
snap_a = lohner_regression_snapshot()
snap_b = lohner_regression_snapshot()
assert snap_a == snap_b
a = [[0.0, -1.0], [1.0, 0.0]]
field = linear_field(a)
jac = constant_jacobian(a)
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
# The jet wrapper must reproduce the same step as lohner_step.
state = LohnerSet.from_box(y0)
jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
plain = lohner_step(field, jac, state, 0.05, 12)
for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
assert left.lo == right.lo and left.hi == right.hi
assert isinstance(budget, WidthBudget)
wrap = naive_vs_lohner_wrapping()
assert wrap["naive"] > wrap["lohner"]
# Existing path still encloses the rotation centre.
box = classic.to_box()
assert box[0].lo <= math.cos(1.0) <= box[0].hipython -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g6_lohner_flow_bit_unchanged -qRead the implementation
def lohner_step_jet(
state: LohnerSet,
field: VectorField,
jac: JacobianEnclosure,
*,
order: int,
h: float,
) -> tuple[LohnerSet, WidthBudget]:
"""Order-``p`` QR-Lohner step. Same update as :func:`lohner_step`."""
if order < 1:
raise ValueError(f"order must be >= 1, got {order}")
if h <= 0.0:
raise ValueError(f"h must be positive, got {h}")
nxt = lohner_step(field, jac, state, h, order)
return nxt, _step_budget(field, jac, state, nxt, h, order)naive_vs_lohner_wrapping
omnibias.core.verified.jet_flow.naive_vs_lohner_wrappingSource ↗naive_vs_lohner_wrapping() -> dict[str, float]Sanity: QR-Lohner still beats naive interval on a rotation.
dict[str, float]Executed regression · g6 lohner flow bit unchanged
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g6_lohner_flow_bit_unchanged() -> None:
snap_a = lohner_regression_snapshot()
snap_b = lohner_regression_snapshot()
assert snap_a == snap_b
a = [[0.0, -1.0], [1.0, 0.0]]
field = linear_field(a)
jac = constant_jacobian(a)
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
classic = lohner_flow(field, jac, y0, 0.05, 20, order=12)
# The jet wrapper must reproduce the same step as lohner_step.
state = LohnerSet.from_box(y0)
jet_state, budget = lohner_step_jet(state, field, jac, order=12, h=0.05)
plain = lohner_step(field, jac, state, 0.05, 12)
for left, right in zip(jet_state.to_box(), plain.to_box(), strict=True):
assert left.lo == right.lo and left.hi == right.hi
assert isinstance(budget, WidthBudget)
wrap = naive_vs_lohner_wrapping()
assert wrap["naive"] > wrap["lohner"]
# Existing path still encloses the rotation centre.
box = classic.to_box()
assert box[0].lo <= math.cos(1.0) <= box[0].hipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g6_lohner_flow_bit_unchanged" -qRead the implementation
def naive_vs_lohner_wrapping() -> dict[str, float]:
"""Sanity: QR-Lohner still beats naive interval on a rotation."""
a = [[0.0, -1.0], [1.0, 0.0]]
y0 = [Interval(0.999, 1.001), Interval(-0.001, 0.001)]
h = 0.05
steps = 40
loh = lohner_flow(linear_field(a), constant_jacobian(a), y0, h, steps, order=12)
naive = naive_interval_flow(a, y0, h, steps, order=12)
return {"lohner": loh.width(), "naive": naive[0].width}named_orbit_problems
omnibias.core.verified.jet_flow.named_orbit_problemsSource ↗named_orbit_problems() -> list[tuple[str, VectorField, JacobianEnclosure, list[float], float]]Three isolated radial Hopf cycles (replayable G4 certificates).
list[tuple[str, VectorField, JacobianEnclosure, list[float], float]]Executed regression · g4 orbit recovery
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g4_orbit_recovery() -> None:
rows = orbit_recovery_report()
assert len(rows) == 3
assert all(row["recovered"] for row in rows), rows
for row in rows:
assert row["jet_enclosure"] is not None
lo, hi = row["jet_enclosure"][0]
assert hi >= lopython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -qRead the implementation
def named_orbit_problems() -> list[tuple[str, VectorField, JacobianEnclosure, list[float], float]]:
"""Three isolated radial Hopf cycles (replayable G4 certificates)."""
out: list[tuple[str, VectorField, JacobianEnclosure, list[float], float]] = []
for mu in (1.0, 0.5, 0.25):
field, jac = radial_hopf(mu)
out.append((f"radial_mu_{mu:g}", field, jac, [math.sqrt(mu)], _TWO_PI))
return outnamed_tower_fields
omnibias.core.verified.jet_flow.named_tower_fieldsSource ↗named_tower_fields() -> list[TowerFieldSpec]Ten activation-dictionary fields for G2 containment.
list[TowerFieldSpec]Executed regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRegression example · g1 width budget on every run
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g1_width_budget_on_every_run -qRead the implementation
def named_tower_fields() -> list[TowerFieldSpec]:
"""Ten activation-dictionary fields for G2 containment."""
return [
TowerFieldSpec("tanh"),
TowerFieldSpec("sigmoid"),
TowerFieldSpec("gaussian"),
TowerFieldSpec("sech"),
TowerFieldSpec("silu"),
TowerFieldSpec("softplus"),
TowerFieldSpec("gelu"),
TowerFieldSpec("tanh", kind="oscillator", stiffness=1.0, damping=0.0),
TowerFieldSpec("sigmoid", kind="oscillator", stiffness=0.8, damping=0.1),
TowerFieldSpec("sech", scale=1.2, bias=-0.25, kind="oscillator"),
]orbit_recovery_report
omnibias.core.verified.jet_flow.orbit_recovery_reportSource ↗orbit_recovery_report() -> list[dict[str, Any]]G4: polluted order-4 proofs fail; exact jet proofs succeed.
list[dict[str, Any]]Executed regression · g4 orbit recovery
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g4_orbit_recovery() -> None:
rows = orbit_recovery_report()
assert len(rows) == 3
assert all(row["recovered"] for row in rows), rows
for row in rows:
assert row["jet_enclosure"] is not None
lo, hi = row["jet_enclosure"][0]
assert hi >= lopython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -qRead the implementation
def orbit_recovery_report() -> list[dict[str, Any]]:
"""G4: polluted order-4 proofs fail; exact jet proofs succeed."""
rows: list[dict[str, Any]] = []
for name, field, jac, x_bar, period in named_orbit_problems():
dirty = widen_jacobian(jac, 4.0)
baseline = prove_periodic_orbit_jet(
field, dirty, x_bar, period, n_steps=40, order=4, radii=(1e-4, 1e-3, 1e-2)
)
jet = prove_periodic_orbit_jet(
field, jac, x_bar, period, n_steps=50, order=14, radii=(1e-5, 1e-4, 1e-3, 1e-2)
)
rows.append(
{
"name": name,
"baseline_exists": baseline.exists,
"jet_exists": jet.exists,
"jet_kappa": jet.kappa,
"jet_enclosure": jet.enclosure,
"recovered": (not baseline.exists) and jet.exists,
}
)
return rowsprove_periodic_orbit_jet
omnibias.core.verified.jet_flow.prove_periodic_orbit_jetSource ↗prove_periodic_orbit_jet(field: VectorField, jac: JacobianEnclosure, x_bar: Sequence[float], period: float, *, n_steps: int=20, order: int=14, radii: Sequence[float]=(1e-06, 1e-05, 0.0001, 0.001, 0.01, 0.05)) -> OrbitProofKrawczyk periodic point of Phi_T, integrated with the jet stepper.
Parameters
| Name | Type & default | Contract |
|---|---|---|
fieldpositional-or-keyword | VectorFieldRequired | See the operation contract and implementation below. |
jacpositional-or-keyword | JacobianEnclosureRequired | See the operation contract and implementation below. |
x_barpositional-or-keyword | Sequence[float]Required | See the operation contract and implementation below. |
periodpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
n_stepskeyword-only | intDefault: 20 | See the operation contract and implementation below. |
orderkeyword-only | intDefault: 14 | See the operation contract and implementation below. |
radiikeyword-only | Sequence[float]Default: (1e-06, 1e-05, 0.0001, 0.001, 0.01, 0.05) | See the operation contract and implementation below. |
OrbitProofExplicit validation & failure cases
- When
period <= 0.0, raisesValueError('period must be positive').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g4 orbit recovery
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g4_orbit_recovery() -> None:
rows = orbit_recovery_report()
assert len(rows) == 3
assert all(row["recovered"] for row in rows), rows
for row in rows:
assert row["jet_enclosure"] is not None
lo, hi = row["jet_enclosure"][0]
assert hi >= lopython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -qRead the implementation
def prove_periodic_orbit_jet(
field: VectorField,
jac: JacobianEnclosure,
x_bar: Sequence[float],
period: float,
*,
n_steps: int = 20,
order: int = 14,
radii: Sequence[float] = (1e-6, 1e-5, 1e-4, 1e-3, 1e-2, 5e-2),
) -> OrbitProof:
"""Krawczyk periodic point of ``Phi_T``, integrated with the jet stepper."""
if period <= 0.0:
raise ValueError("period must be positive")
n = len(x_bar)
h = period / n_steps
failure = (ValueError, RuntimeError, OverflowError, ZeroDivisionError)
def func(box: list[Interval]) -> list[Interval]:
end, _, _ = variational_flow_jet(field, jac, box, h, n_steps, order)
out = end.to_box()
return [out[i] - box[i] for i in range(n)]
def jacobian(box: list[Interval]) -> IntervalMatrix:
_, fundamental, _ = variational_flow_jet(field, jac, box, h, n_steps, order)
return mat_sub(fundamental, identity_matrix(n))
try:
j_center = jacobian([Interval.point(v) for v in x_bar])
a_inv = _float_inverse([[x.mid for x in row] for row in j_center])
except failure:
a_inv = None
if a_inv is None:
return OrbitProof(False, period, tuple(x_bar), None, None, None)
budget: WidthBudget | None = None
for radius in radii:
try:
cert = krawczyk_certificate(func, jacobian, list(x_bar), a_inv, radius)
_, _, budget = variational_flow_jet(
field, jac, [Interval.point(v) for v in x_bar], h, n_steps, order
)
except failure:
continue
if cert is not None:
return OrbitProof(
True,
period,
tuple(x_bar),
cert.enclosure,
cert.kappa,
budget,
)
return OrbitProof(False, period, tuple(x_bar), None, None, budget)radial_hopf
omnibias.core.verified.jet_flow.radial_hopfSource ↗radial_hopf(mu: float=1.0) -> tuple[VectorField, JacobianEnclosure]Scalar radial Hopf map r' = mu r - r^3 (isolated cycle at sqrt(mu)).
Parameters
| Name | Type & default | Contract |
|---|---|---|
mupositional-or-keyword | floatDefault: 1.0 | See the operation contract and implementation below. |
tuple[VectorField, JacobianEnclosure]Executed regression · g3 horizon extension
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g3_horizon_extension" -qRead the implementation
def radial_hopf(mu: float = 1.0) -> tuple[VectorField, JacobianEnclosure]:
"""Scalar radial Hopf map ``r' = mu r - r^3`` (isolated cycle at ``sqrt(mu)``)."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
r = series[0]
return [r * mu - r * r * r]
def jac(box: Sequence[Interval]) -> IntervalMatrix:
r = box[0]
return [[Interval.point(mu) - Interval.point(3.0) * r.pow_int(2)]]
return field, jacriccati_field
omnibias.core.verified.jet_flow.riccati_fieldSource ↗riccati_field() -> VectorFieldx' = x^2. Solution 1/(1-t) from x(0)=1 blows up at t=1.
VectorFieldExecuted regression · g5 singularity step soundness
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g5_singularity_step_soundness() -> None:
rows = singularity_step_report()
assert len(rows) == 3
assert all(row["sound"] for row in rows), rows
riccati = next(row for row in rows if row["name"] == "riccati")
assert riccati["step"] <= 1.0
tan_row = next(row for row in rows if row["name"] == "tan")
assert tan_row["step"] <= 0.5 * math.pipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g5_singularity_step_soundness" -qRead the implementation
def riccati_field() -> VectorField:
"""``x' = x^2``. Solution ``1/(1-t)`` from ``x(0)=1`` blows up at ``t=1``."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
x = series[0]
return [x * x]
return fieldrun_schema_errors
omnibias.core.verified.jet_flow.run_schema_errorsSource ↗run_schema_errors(run: ValidatedRun) -> list[str]The module contract describes the context for this operation. Its signature, explicit validation, return expressions, and implementation are recorded below.
Parameters
| Name | Type & default | Contract |
|---|---|---|
runpositional-or-keyword | ValidatedRunRequired | See the operation contract and implementation below. |
list[str]Executed regression · g1 width budget on every run
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g1_width_budget_on_every_run" -qRead the implementation
def run_schema_errors(run: ValidatedRun) -> list[str]:
errors: list[str] = []
if run.budget.dominant not in {"truncation", "jacobian", "wrapping", "rounding"}:
errors.append("dominant_missing")
if run.horizon <= 0.0:
errors.append("horizon_nonpositive")
return errorsseal_run
omnibias.core.verified.jet_flow.seal_runSource ↗seal_run(run: ValidatedRun) -> dict[str, object]Hash-sealed v1 certificate. Reserved kernel keys are never supplied.
Parameters
| Name | Type & default | Contract |
|---|---|---|
runpositional-or-keyword | ValidatedRunRequired | See the operation contract and implementation below. |
dict[str, object]Executed regression · g1 width budget on every run
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g1_width_budget_on_every_run" -qRead the implementation
def seal_run(run: ValidatedRun) -> dict[str, object]:
"""Hash-sealed v1 certificate. Reserved kernel keys are never supplied."""
from omnibias.core.verified.enclosure_collapse import diagnose_width
box = run.state.to_box()
return dict(
make_certificate(
claim="finite-horizon Lohner enclosure of one trajectory",
payload={
"schema": SCHEMA_VERSION,
"horizon": run.horizon,
"n_steps": run.n_steps,
"order": run.order,
"width": run.width,
"box": [(iv.lo, iv.hi) for iv in box],
"budget": run.budget.to_payload(),
"diagnosis": diagnose_width(run.budget).to_payload(),
"disclaimer": DISCLAIMER,
},
honesty=_seal_honesty(),
)
)singularity_step_report
omnibias.core.verified.jet_flow.singularity_step_reportSource ↗singularity_step_report() -> list[dict[str, Any]]G5: suggested steps stay strictly inside the known radius.
list[dict[str, Any]]Executed regression · g5 singularity step soundness
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g5_singularity_step_soundness() -> None:
rows = singularity_step_report()
assert len(rows) == 3
assert all(row["sound"] for row in rows), rows
riccati = next(row for row in rows if row["name"] == "riccati")
assert riccati["step"] <= 1.0
tan_row = next(row for row in rows if row["name"] == "tan")
assert tan_row["step"] <= 0.5 * math.pipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g5_singularity_step_soundness" -qRegression example · g3 horizon extension
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g3_horizon_extension() -> None:
rows = horizon_report()
assert len(rows) == 10
assert all("ratio" in row for row in rows)
wins = sum(1 for row in rows if row["win"])
assert wins == 10, rowspython -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g3_horizon_extension -qRead the implementation
def singularity_step_report() -> list[dict[str, Any]]:
"""G5: suggested steps stay strictly inside the known radius."""
cases = [
("riccati", riccati_field(), [Interval.point(1.0)], 1.0),
("tan", tan_field(), [Interval.point(0.0)], 0.5 * math.pi),
("exp", exp_field(), [Interval.point(1.0)], math.inf),
]
rows: list[dict[str, Any]] = []
for name, field, y0, true_r in cases:
state = LohnerSet.from_box(y0)
step = adaptive_step_from_singularity(field, state, order=16, safety=0.5, max_step=1.0)
finite = math.isfinite(true_r)
ok = step <= true_r if finite else 0.0 < step <= 1.0
rows.append(
{
"name": name,
"step": step,
"true_radius": true_r if finite else None,
"sound": ok,
}
)
return rowstan_field
omnibias.core.verified.jet_flow.tan_fieldSource ↗tan_field() -> VectorFieldx' = 1 + x^2. Solution tan(t) from x(0)=0 blows up at π/2.
VectorFieldExecuted regression · g5 singularity step soundness
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g5_singularity_step_soundness() -> None:
rows = singularity_step_report()
assert len(rows) == 3
assert all(row["sound"] for row in rows), rows
riccati = next(row for row in rows if row["name"] == "riccati")
assert riccati["step"] <= 1.0
tan_row = next(row for row in rows if row["name"] == "tan")
assert tan_row["step"] <= 0.5 * math.pipython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g5_singularity_step_soundness" -qRead the implementation
def tan_field() -> VectorField:
"""``x' = 1 + x^2``. Solution ``tan(t)`` from ``x(0)=0`` blows up at ``π/2``."""
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
x = series[0]
return [x * x + 1.0]
return fieldtower_field
omnibias.core.verified.jet_flow.tower_fieldSource ↗tower_field(spec: TowerFieldSpec) -> VectorFieldClosed-form activation vector field for spec.
Parameters
| Name | Type & default | Contract |
|---|---|---|
specpositional-or-keyword | TowerFieldSpecRequired | See the operation contract and implementation below. |
VectorFieldExecuted regression · coefficient arithmetic chooses interval
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_coefficient_arithmetic_chooses_interval() -> None:
report = coefficient_arithmetic_report()
assert report["choice"] == "interval"
assert report["tm_required"] is Falsepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_coefficient_arithmetic_chooses_interval" -qRegression example · g1 width budget on every run
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g1_width_budget_on_every_run -qRead the implementation
def tower_field(spec: TowerFieldSpec) -> VectorField:
"""Closed-form activation vector field for ``spec``."""
scale = Interval.point(spec.scale)
bias = Interval.point(spec.bias)
stiff = Interval.point(spec.stiffness)
damp = Interval.point(spec.damping)
name = spec.name
def _sigma(series: TaylorSeries) -> TaylorSeries:
u = [scale * coeff for coeff in series.coeffs]
u[0] = u[0] + bias
tower = sigma_tower_interval(name, u[0], len(u) - 1)
return TaylorSeries(compose_jet(u, list(tower)))
if spec.kind == "scalar":
def field(series: list[TaylorSeries]) -> list[TaylorSeries]:
return [_sigma(series[0])]
return field
def osc(series: list[TaylorSeries]) -> list[TaylorSeries]:
x, y = series[0], series[1]
return [y, _sigma(x) * (-stiff) + y * (-damp)]
return osctower_jacobian
omnibias.core.verified.jet_flow.tower_jacobianSource ↗tower_jacobian(spec: TowerFieldSpec) -> JacobianEnclosureExact closed-form Jacobian enclosure. Width is rounding plus the box.
Parameters
| Name | Type & default | Contract |
|---|---|---|
specpositional-or-keyword | TowerFieldSpecRequired | See the operation contract and implementation below. |
JacobianEnclosureExecuted regression · g2 jacobian containment
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g2_jacobian_containment() -> None:
report = jacobian_containment_report(n_boxes=1000, seed=3)
assert report["fields"] == 10
assert report["checked"] == 10000
assert report["misses"] == 0
assert report["containment"] is Truepython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g2_jacobian_containment" -qRegression example · g1 width budget on every run
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g1_width_budget_on_every_run() -> None:
spec = named_tower_fields()[0]
run = lohner_flow_jet(
tower_field(spec),
tower_jacobian(spec),
[Interval(0.2, 0.3)],
0.05,
8,
order=8,
)
assert run.budget.dominant in {"truncation", "jacobian", "wrapping", "rounding"}
assert run.budget.total >= 0.0
assert run_schema_errors(run) == []
sealed = seal_run(run)
assert "theorem_prover_verified" not in sealed["honesty"]
assert honesty_payload()["theorem_prover_verified"] is False
assert "finite-horizon enclosure" in DISCLAIMER
diagnosis = sealed["payload"]["diagnosis"]
assert diagnosis["dominant"] == run.budget.dominant
assert diagnosis["action"] in {"raise_order", "subdivide", "shrink_step", "stop_floor"}
if diagnosis["dominant"] == "jacobian":
assert diagnosis["action"] == "shrink_step"
assert "bias" not in diagnosis["reason"]python -m pytest packages/omnibias-core/tests/verified/test_jet_flow.py -k test_g1_width_budget_on_every_run -qRead the implementation
def tower_jacobian(spec: TowerFieldSpec) -> JacobianEnclosure:
"""Exact closed-form Jacobian enclosure. Width is rounding plus the box."""
scale = Interval.point(spec.scale)
bias = Interval.point(spec.bias)
stiff = Interval.point(spec.stiffness)
damp = Interval.point(spec.damping)
name = spec.name
zero = Interval.point(0.0)
one = Interval.point(1.0)
if spec.kind == "scalar":
def jac_s(box: Sequence[Interval]) -> IntervalMatrix:
arg = scale * box[0] + bias
return [[scale * sigma_tower_interval(name, arg, 1)[1]]]
return jac_s
def jac_o(box: Sequence[Interval]) -> IntervalMatrix:
arg = scale * box[0] + bias
prime = sigma_tower_interval(name, arg, 1)[1]
return [[zero, one], [(-stiff) * scale * prime, -damp]]
return jac_ovariational_flow_jet
omnibias.core.verified.jet_flow.variational_flow_jetSource ↗variational_flow_jet(field: VectorField, jac: JacobianEnclosure, y0: Sequence[IntervalLike], h: float, n_steps: int, order: int) -> tuple[LohnerSet, IntervalMatrix, WidthBudget]State plus fundamental matrix, using the jet stepper.
Parameters
| Name | Type & default | Contract |
|---|---|---|
fieldpositional-or-keyword | VectorFieldRequired | See the operation contract and implementation below. |
jacpositional-or-keyword | JacobianEnclosureRequired | See the operation contract and implementation below. |
y0positional-or-keyword | Sequence[IntervalLike]Required | See the operation contract and implementation below. |
hpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
n_stepspositional-or-keyword | intRequired | See the operation contract and implementation below. |
orderpositional-or-keyword | intRequired | See the operation contract and implementation below. |
tuple[LohnerSet, IntervalMatrix, WidthBudget]Explicit validation & failure cases
- When
n_steps < 1, raisesValueError('n_steps must be >= 1').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g4 orbit recovery
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g4_orbit_recovery() -> None:
rows = orbit_recovery_report()
assert len(rows) == 3
assert all(row["recovered"] for row in rows), rows
for row in rows:
assert row["jet_enclosure"] is not None
lo, hi = row["jet_enclosure"][0]
assert hi >= lopython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -qRead the implementation
def variational_flow_jet(
field: VectorField,
jac: JacobianEnclosure,
y0: Sequence[IntervalLike],
h: float,
n_steps: int,
order: int,
) -> tuple[LohnerSet, IntervalMatrix, WidthBudget]:
"""State plus fundamental matrix, using the jet stepper."""
if n_steps < 1:
raise ValueError("n_steps must be >= 1")
state = LohnerSet.from_box(y0)
fundamental = identity_matrix(len(state.center))
budget = _zero_budget()
for _ in range(n_steps):
box = state.to_box()
z_encl = _apriori_enclosure(field, box, h)
j_step = interval_matrix_exp(_scale_matrix(jac(z_encl), h), order=max(order, 8))
state, piece = lohner_step_jet(state, field, jac, order=order, h=h)
fundamental = matmul(j_step, fundamental)
budget = _merge_budget(budget, piece)
return state, fundamental, budgetwiden_jacobian
omnibias.core.verified.jet_flow.widen_jacobianSource ↗widen_jacobian(jac: JacobianEnclosure, delta: float) -> JacobianEnclosureAdd a symmetric interval pad. The polluted baseline for G4 / G3.
Parameters
| Name | Type & default | Contract |
|---|---|---|
jacpositional-or-keyword | JacobianEnclosureRequired | See the operation contract and implementation below. |
deltapositional-or-keyword | floatRequired | See the operation contract and implementation below. |
JacobianEnclosureExplicit validation & failure cases
- When
delta < 0.0, raisesValueError(f'delta must be >= 0, got {delta}').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · g4 orbit recovery
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_g4_orbit_recovery() -> None:
rows = orbit_recovery_report()
assert len(rows) == 3
assert all(row["recovered"] for row in rows), rows
for row in rows:
assert row["jet_enclosure"] is not None
lo, hi = row["jet_enclosure"][0]
assert hi >= lopython -m pytest "packages/omnibias-core/tests/verified/test_jet_flow.py::test_g4_orbit_recovery" -qRead the implementation
def widen_jacobian(jac: JacobianEnclosure, delta: float) -> JacobianEnclosure:
"""Add a symmetric interval pad. The polluted baseline for G4 / G3."""
if delta < 0.0:
raise ValueError(f"delta must be >= 0, got {delta}")
pad = Interval(-delta, delta)
def polluted(box: Sequence[Interval]) -> IntervalMatrix:
return [[entry + pad for entry in row] for row in jac(box)]
return polluted