aether_quant.formal¶

Differential cases computed by the Lean 4 models in formal/ (aq prove --regen-cases): run a Python function on a case's input and compare with its expected to check it still matches the verified model.

cases_dir ¶

cases_dir() -> Path

The folder of differential cases shipped with the package.

decode_rational ¶

decode_rational(value: Mapping[str, int] | None) -> Fraction | None

{"num": n, "den": d} -> Fraction; JSON null -> None.

load_cases ¶

load_cases(target: str) -> dict[str, Any]

One target's cases file (input, expected and the spec digest).

spec_sha256 ¶

spec_sha256(spec_root: Path, spec_files: list[str]) -> str

sha256 over the spec files' bytes in listed order (line endings normalised to LF).

targets ¶

targets() -> list[str]

The names of the targets with shipped cases.

to_float ¶

to_float(value: Mapping[str, int] | None) -> float | None

A case's {"num", "den"} rational as a float; None for null.