UPDE — PHA-C Lean Kinematic Proof Obligation¶

PHACKinematicProofObligation is the review-only bridge between a verified runtime PHACAcceptanceRecord and the Lean module SPOFormal.Kinematic. It converts the accepted PHA-C trajectory envelope into fixed-point natural-number fields that match KinematicBounds, then signs the manifest with a deterministic SHA-256 hash.

Formal guarantee boundary¶

The Lean files prove arithmetic certificate predicates over the fixed-point manifest fields named below. They do not prove that a live plant, accelerator, hardware bridge, QPU, neuromorphic target, or external controller will remain safe. The runtime still needs sensor calibration, actuator bounds, deployment network controls, and operator approval before any result can be promoted from review evidence to operational evidence.

Current release guarantees are therefore scoped as follows:

Surface	What is proven or checked	What is not claimed
Lean `SPOFormal.Kinematic`	fixed-point kinematic, sampled-rate, phase-budget, and acceptance certificate implications	real-analysis proof of the physical system or hardware actuation safety
Python verifier	schema, theorem names, fixed-point arithmetic replay, hash replay, and disabled-execution flags	independent theorem proving
Rust/Go/Julia/Mojo PHA-C rows	source-contract parity and benchmark/reference gates where toolchains are available	universal native execution across every downstream language row
Release docs	review-only handoff evidence for MIF/FRC consumers	automatic permission to actuate live systems

The obligation does not execute Lean, write to hardware, mutate a supervisor, or change a coupling policy. It records the exact theorem and Boolean certificate predicate that a reviewer or CI proof gate must use:

Lean module: SPOFormal.Kinematic
Predicate: KinematicBounds.budgetCertificate
Theorem: budget_certificate_discharges_budget
Continuous-envelope module: SPOFormal.Continuous
Continuous predicate: ContinuousEnvelopeBounds.budgetCertificate
Continuous theorem: continuous_envelope_certificate_discharges_horizon
Phase-budget module: SPOFormal.Kinematic
Phase predicate: PhaseBudgetBounds.budgetCertificate
Phase theorem: phase_budget_certificate_discharges_phase_lock
Combined acceptance predicate: KinematicBounds.acceptanceCertificate
Combined acceptance theorem: acceptance_certificate_discharges_runtime_preconditions

Use cases¶

Use this manifest when the PHA-C acceptance chain needs a formal review bridge:

MIF/FRC handoff packages that need fixed-point assumptions to specialise into downstream constants;
release evidence that must prove runtime PHA-C acceptance has a named Lean theorem target, not only empirical trajectory hashes;
benchmark gates that must fail when the accepted trajectory no longer fits the finite-horizon Gronwall merge-window certificate;
Studio or audit panels that need a compact proof-obligation hash without exposing raw trajectory arrays.

Fixed-point mapping¶

The builder first verifies the source PHACAcceptanceRecord, then projects the runtime envelope into integer units:

Manifest field	Runtime source	Lean role
`time_step_s`	accepted integration `dt`	sampled-rate time step
`fixed_point_time_scale_s`	manifest time scale, default `1e-6`	sampled-rate fixed-point clock
`time_scale_units_per_second`	`ceil(1 / fixed_point_time_scale_s)`	sampled-rate denominator
`time_step_units`	`ceil(time_step_s / fixed_point_time_scale_s)`	sampled-rate numerator
`horizon_time_units`	`horizon_steps * time_step_units`	reviewed horizon duration
`initial_tolerance_units`	max observed spatial dispersion	`KinematicBounds.initialTolerance`
`lipschitz_step_gain_units`	explicit control, default `0`	`KinematicBounds.lipschitzStepGain`
`relative_velocity_rate_bound_units_per_second`	predictive slack divided by `dt`	`SampledRateKinematicBounds.relativeVelocityRateBound`
`relative_velocity_step_bound_units`	explicit predictive slack, default `0`	`KinematicBounds.relativeVelocityStepBound`
`configured_coupling_residual_step_bound_units`	explicit predictive residual slack, default `0`	residual-bound provenance
`coupling_residual_rate_bound_units_per_second`	max of configured residual slack and observed moving-frame residual, divided by `dt`	`SampledRateKinematicBounds.couplingResidualRateBound`
`coupling_residual_step_bound_units`	max of configured residual slack and observed moving-frame residual	`KinematicBounds.couplingResidualStepBound`
`continuous_drive_rate_bound_units_per_second`	velocity-rate plus residual-rate bound	`ContinuousEnvelopeBounds.driveRateBound`
`continuous_horizon_drive_bound_units`	sampled continuous drive over `horizon_time_units`	`ContinuousEnvelopeBounds.sampledDriveBoundAt`
`continuous_linear_budget_units`	initial dispersion plus sampled horizon drive	`ContinuousEnvelopeBounds.budgetAt`
`continuous_margin_units`	merge tolerance minus continuous budget	`ContinuousEnvelopeBounds.budgetCertificate`
`merge_window_tolerance_units`	spatial merge tolerance	`KinematicBounds.mergeWindowTolerance`
`horizon_steps`	accepted PHA-C step count	`KinematicBounds.horizonSteps`
`phase_tolerance_units`	accepted phase tolerance	phase-lock certificate input
`max_phase_dispersion_units`	max observed phase dispersion	replayed phase evidence
`configured_phase_drift_bound_units`	explicit predictive phase-drift slack, default `0`	phase-bound provenance
`phase_budget_units`	observed dispersion plus configured phase drift	phase-lock budget
`phase_margin_units`	phase tolerance minus phase budget	phase-lock certificate margin
`phase_budget_discharged`	`phase_budget_units <= phase_tolerance_units`	`PhaseBudgetBounds.budgetCertificate`
`acceptance_kinematic_equations_validated`	verified acceptance record preserved final-position, velocity, and path-length equations	runtime-to-formal acceptance precondition
`acceptance_kinematic_summary_replay_tolerance`	replay tolerance inherited from `PHACAcceptanceRecord`	runtime-to-formal tolerance provenance
`acceptance_kinematic_summary_replay_tolerance_units`	fixed-point replay tolerance	`AcceptanceKinematicReplayBounds.summaryReplayTolerance`
`acceptance_kinematic_summary_replay_tolerance_limit_units`	fixed-point replay tolerance limit	`AcceptanceKinematicReplayBounds.summaryReplayToleranceLimit`
`acceptance_replay_certificate_discharged`	equation flag plus tolerance bound	`AcceptanceKinematicReplayBounds.replayCertificate`
`acceptance_certificate_discharged`	spatial budget plus phase budget plus replay certificate	`KinematicBounds.acceptanceCertificate`

The default is a replay certificate. The observed spatial dispersion already includes the accepted moving-frame trajectory, while the residual term proves the ballistic coordinate update was mechanically valid. Downstream predictive lanes can provide non-zero relative_velocity_step_bound_m and non-zero coupling_residual_step_bound_m values when they need a reviewed residual envelope beyond the observed replay residual. The verifier requires the configured residual units to fit inside the sampled residual bound before the same Lean theorem can certify a future horizon rather than the replay envelope. Non-zero lipschitz_step_gain_units can then be added for finite-horizon growth.

The phase side is also explicit. Downstream lanes can provide phase_drift_bound_rad when the reviewed handoff must budget future phase drift in addition to the accepted replay dispersion. The manifest records that slack as configured_phase_drift_bound_units, records phase_budget_units = max_phase_dispersion_units + configured_phase_drift_bound_units, and derives phase_margin_units from the budget rather than from replay dispersion alone. The manifest names the Lean PhaseBudgetBounds.budgetCertificate predicate and phase_budget_certificate_discharges_phase_lock theorem so the phase budget is reviewed by a formal fixed-point mirror instead of only by Python arithmetic. The Boolean phase_budget_discharged must match that theorem condition exactly before the combined PHA-C proof obligations can discharge.

The manifest also carries acceptance_kinematic_equations_validated and acceptance_kinematic_summary_replay_tolerance. These fields bind the Lean obligation to the verified acceptance record's final-position, maximum-velocity, and path-length equation replay, so a formal manifest cannot be detached from mechanically valid moving-frame summary evidence.

The Lean mirror now names the same requirement as AcceptanceKinematicReplayBounds.replayCertificate and folds it into KinematicBounds.acceptanceCertificate. A release reviewer can therefore check one Boolean fixed-point acceptance certificate that joins the spatial Gronwall budget, phase-lock budget, and runtime equation-replay provenance instead of reviewing the replay flag as loose metadata. The Python manifest now records acceptance_certificate_predicate, acceptance_certificate_theorem, acceptance_replay_certificate_discharged, and acceptance_certificate_discharged, and the verifier recomputes each field from the same fixed-point units before accepting the manifest hash.

For non-zero gain, the runtime manifest replays the Lean recurrence previous + gain * previous + drive, records the terminal gronwall_budget_units, records the signed gronwall_budget_margin_units, and hashes the full budget trace as gronwall_budget_trace_sha256. The legacy linear_budget_units field remains as the zero-gain reference budget; the merge-window margin is now derived from the Gronwall terminal budget.

For continuous-rate handoffs, the manifest also records a sampled-rate mirror: per-second relative-velocity and residual bounds are sampled through time_step_units / time_scale_units_per_second before they enter the discrete Lean budget. The Lean side names this bridge SampledRateKinematicBounds and proves that a sampled-rate certificate discharges the same finite-horizon merge-window budget after conversion to KinematicBounds.

The manifest also records the continuous-envelope theorem target. That layer samples the same per-second rates over horizon_time_units, records the continuous horizon drive, and requires the signed continuous margin to be non-negative before proof_obligations_discharged can be true. The Lean side names this boundary ContinuousEnvelopeBounds; it is a dependency-light fixed-point continuous envelope, not a Mathlib real-analysis proof.

Minimal example¶

from scpn_phase_orchestrator.upde.pha_c_acceptance import (
    build_pha_c_acceptance_record,
)
from scpn_phase_orchestrator.upde.pha_c_formal_obligation import (
    build_pha_c_kinematic_proof_obligation,
    verify_pha_c_kinematic_proof_obligation,
)

record = build_pha_c_acceptance_record(...)
obligation = build_pha_c_kinematic_proof_obligation(record)

assert obligation.lean_theorem == "budget_certificate_discharges_budget"
assert obligation.acceptance_certificate_predicate == (
    "KinematicBounds.acceptanceCertificate"
)
assert obligation.acceptance_certificate_theorem == (
    "acceptance_certificate_discharges_runtime_preconditions"
)
assert obligation.acceptance_replay_certificate_discharged
assert obligation.acceptance_certificate_discharged
assert obligation.proof_obligations_discharged
verify_pha_c_kinematic_proof_obligation(obligation)

Verification boundary¶

verify_pha_c_kinematic_proof_obligation(...) checks:

exact schema, evidence kind, claim boundary, Lean kinematic, continuous, and phase-budget module, predicate, and theorem names;
review-only flags: execution_disabled=True and actuating=False;
finite positive metric and phase fixed-point scales;
finite positive time scale and accepted time-step sampling fields;
natural-number fields and the Lean equations for drive, linear zero-gain reference budget, Gronwall budget trace, terminal budget, and merge-window margin;
continuous-envelope theorem metadata, drive-rate sum, horizon-drive replay, continuous budget, and continuous margin;
configured residual-bound provenance and its fit inside the sampled residual drive bound;
configured phase-drift provenance, phase-budget replay, and phase tolerance margin consistency;
phase_budget_discharged replay against the Lean PhaseBudgetBounds.budgetCertificate condition;
acceptance_kinematic_equations_validated replay against the verified acceptance record's moving-frame summary equations;
fixed-point replay-tolerance units, replay certificate discharge, and the combined KinematicBounds.acceptanceCertificate discharge;
lower-case SHA-256 fields; and
canonical manifest hash replay.

If proof_obligations_discharged disagrees with the fixed-point certificate math, verification fails closed.

The public serialisation helpers PHACKinematicProofObligation.to_dict() and pha_c_kinematic_proof_obligation_to_dict(...) call the same verifier before returning a manifest. A stale or tampered dataclass therefore cannot publish a canonical JSON payload without replaying the fixed-point certificate checks and hash validation first.

PHACKinematicProofObligation `dataclass` ¶

PHACKinematicProofObligation(
    schema_version: str,
    evidence_kind: str,
    claim_boundary: str,
    acceptance_claim_boundary: str,
    execution_disabled: bool,
    actuating: bool,
    lean_module: str,
    lean_certificate_predicate: str,
    lean_theorem: str,
    continuous_lean_module: str,
    continuous_certificate_predicate: str,
    continuous_theorem: str,
    phase_lean_module: str,
    phase_certificate_predicate: str,
    phase_theorem: str,
    acceptance_certificate_predicate: str,
    acceptance_certificate_theorem: str,
    fixed_point_scale_m: float,
    fixed_point_scale_rad: float,
    fixed_point_time_scale_s: float,
    time_step_s: float,
    time_scale_units_per_second: int,
    time_step_units: int,
    horizon_time_units: int,
    initial_tolerance_units: int,
    lipschitz_step_gain_units: int,
    relative_velocity_rate_bound_units_per_second: int,
    relative_velocity_step_bound_units: int,
    configured_coupling_residual_step_bound_units: int,
    coupling_residual_rate_bound_units_per_second: int,
    coupling_residual_step_bound_units: int,
    continuous_drive_rate_bound_units_per_second: int,
    continuous_horizon_drive_bound_units: int,
    continuous_linear_budget_units: int,
    continuous_margin_units: int,
    drive_bound_units: int,
    merge_window_tolerance_units: int,
    horizon_steps: int,
    linear_budget_units: int,
    gronwall_budget_units: int,
    gronwall_budget_margin_units: int,
    gronwall_budget_trace_sha256: str,
    window_budget_margin_units: int,
    phase_tolerance_units: int,
    max_phase_dispersion_units: int,
    configured_phase_drift_bound_units: int,
    phase_budget_units: int,
    phase_margin_units: int,
    phase_budget_discharged: bool,
    acceptance_kinematic_equations_validated: bool,
    acceptance_kinematic_summary_replay_tolerance: float,
    acceptance_kinematic_summary_replay_tolerance_units: int,
    acceptance_kinematic_summary_replay_tolerance_limit_units: int,
    acceptance_replay_certificate_discharged: bool,
    acceptance_certificate_discharged: bool,
    observed_velocity_step_units: int,
    kinematic_residual_units: int,
    path_length_units: int,
    max_spatial_dispersion_units: int,
    continuous_envelope_discharged: bool,
    proof_obligations_discharged: bool,
    acceptance_sha256: str,
    timeline_sha256: str,
    record_sha256: str,
)

Review-only fixed-point obligations linked to the Lean kinematic proof.

Methods:¶

to_dict ¶

to_dict() -> dict[str, bool | float | int | str]

Return a verified JSON-safe canonical representation.

Returns¶

dict[str, bool | float | int | str] The verified JSON-safe canonical representation.

Source code in src/scpn_phase_orchestrator/upde/pha_c_formal_obligation.py

def to_dict(self) -> dict[str, bool | float | int | str]:
    """Return a verified JSON-safe canonical representation.

    Returns
    -------
    dict[str, bool | float | int | str]
        The verified JSON-safe canonical representation.
    """
    return pha_c_kinematic_proof_obligation_to_dict(self)

build_pha_c_kinematic_proof_obligation ¶

build_pha_c_kinematic_proof_obligation(
    record: PHACAcceptanceRecord,
    *,
    fixed_point_scale_m: float = PHA_C_FORMAL_DEFAULT_SCALE_M,
    fixed_point_scale_rad: float = PHA_C_FORMAL_DEFAULT_SCALE_RAD,
    fixed_point_time_scale_s: float = PHA_C_FORMAL_DEFAULT_TIME_SCALE_S,
    relative_velocity_step_bound_m: float = 0.0,
    coupling_residual_step_bound_m: float = 0.0,
    phase_drift_bound_rad: float = 0.0,
    lipschitz_step_gain_units: int = 0,
) -> PHACKinematicProofObligation

Project a verified PHA-C acceptance record into Lean proof obligations.

The default obligation is a replay certificate: the maximum observed spatial dispersion is already measured over the accepted trajectory, so the Lean drive term only includes explicitly supplied future relative-velocity slack and the signed moving-frame residual. MIF/FRC specialisations can provide non-zero relative_velocity_step_bound_m and coupling_residual_step_bound_m, phase_drift_bound_rad, and lipschitz_step_gain_units values when they want a predictive finite-horizon Gronwall certificate instead of a replay-only envelope.

Parameters¶

record : PHACAcceptanceRecord The PHA-C record to operate on. fixed_point_scale_m : float Spatial fixed-point scale in metres. fixed_point_scale_rad : float Phase fixed-point scale in radians. fixed_point_time_scale_s : float Temporal fixed-point scale in seconds. relative_velocity_step_bound_m : float Per-step relative-velocity bound in metres. coupling_residual_step_bound_m : float Per-step coupling-residual bound in metres. phase_drift_bound_rad : float Per-step phase-drift bound in radians. lipschitz_step_gain_units : int Lipschitz step-gain bound in dimensionless integer units.

Returns¶

PHACKinematicProofObligation The Lean proof-obligation projection of the acceptance record.

Source code in src/scpn_phase_orchestrator/upde/pha_c_formal_obligation.py

def build_pha_c_kinematic_proof_obligation(
    record: PHACAcceptanceRecord,
    *,
    fixed_point_scale_m: float = PHA_C_FORMAL_DEFAULT_SCALE_M,
    fixed_point_scale_rad: float = PHA_C_FORMAL_DEFAULT_SCALE_RAD,
    fixed_point_time_scale_s: float = PHA_C_FORMAL_DEFAULT_TIME_SCALE_S,
    relative_velocity_step_bound_m: float = 0.0,
    coupling_residual_step_bound_m: float = 0.0,
    phase_drift_bound_rad: float = 0.0,
    lipschitz_step_gain_units: int = 0,
) -> PHACKinematicProofObligation:
    """Project a verified PHA-C acceptance record into Lean proof obligations.

    The default obligation is a replay certificate: the maximum observed
    spatial dispersion is already measured over the accepted trajectory, so the
    Lean drive term only includes explicitly supplied future relative-velocity
    slack and the signed moving-frame residual. MIF/FRC specialisations can
    provide non-zero ``relative_velocity_step_bound_m`` and
    ``coupling_residual_step_bound_m``, ``phase_drift_bound_rad``, and
    ``lipschitz_step_gain_units`` values when they want a predictive
    finite-horizon Gronwall certificate instead of a replay-only envelope.

    Parameters
    ----------
    record : PHACAcceptanceRecord
        The PHA-C record to operate on.
    fixed_point_scale_m : float
        Spatial fixed-point scale in metres.
    fixed_point_scale_rad : float
        Phase fixed-point scale in radians.
    fixed_point_time_scale_s : float
        Temporal fixed-point scale in seconds.
    relative_velocity_step_bound_m : float
        Per-step relative-velocity bound in metres.
    coupling_residual_step_bound_m : float
        Per-step coupling-residual bound in metres.
    phase_drift_bound_rad : float
        Per-step phase-drift bound in radians.
    lipschitz_step_gain_units : int
        Lipschitz step-gain bound in dimensionless integer units.

    Returns
    -------
    PHACKinematicProofObligation
        The Lean proof-obligation projection of the acceptance record.
    """
    verified_record = verify_pha_c_acceptance_record(record)
    scale_m = _validate_positive_scale(fixed_point_scale_m, name="fixed_point_scale_m")
    scale_rad = _validate_positive_scale(
        fixed_point_scale_rad,
        name="fixed_point_scale_rad",
    )
    time_scale = _validate_positive_scale(
        fixed_point_time_scale_s,
        name="fixed_point_time_scale_s",
    )
    time_step_s = _validate_positive_scale(verified_record.dt, name="time_step_s")
    time_scale_units_per_second = _validate_int(
        _ceil_positive_ratio_units(
            1.0,
            time_scale,
            name="time_scale_units_per_second",
        ),
        name="time_scale_units_per_second",
        minimum=1,
    )
    time_step_units = _validate_int(
        _ceil_positive_ratio_units(
            time_step_s,
            time_scale,
            name="time_step_units",
        ),
        name="time_step_units",
        minimum=1,
    )
    horizon_steps = _validate_int(
        verified_record.step_count,
        name="step_count",
        minimum=1,
    )
    horizon_time_units = horizon_steps * time_step_units
    gain_units = _validate_int(
        lipschitz_step_gain_units,
        name="lipschitz_step_gain_units",
        minimum=0,
    )
    raw_relative_velocity_units = _nonnegative_units(
        relative_velocity_step_bound_m,
        scale=scale_m,
        name="relative_velocity_step_bound_m",
    )
    configured_residual_m = _validate_nonnegative_scalar(
        coupling_residual_step_bound_m,
        name="coupling_residual_step_bound_m",
    )
    observed_residual_m = _validate_nonnegative_scalar(
        verified_record.kinematic_residual_max_m,
        name="kinematic_residual_max_m",
    )
    configured_residual_units = _nonnegative_units(
        configured_residual_m,
        scale=scale_m,
        name="coupling_residual_step_bound_m",
    )
    observed_residual_units = _nonnegative_units(
        observed_residual_m,
        scale=scale_m,
        name="kinematic_residual_max_m",
    )
    raw_residual_units = max(configured_residual_units, observed_residual_units)
    residual_bound_m = max(configured_residual_m, observed_residual_m)
    relative_velocity_rate_units = max(
        _nonnegative_units(
            relative_velocity_step_bound_m / time_step_s,
            scale=scale_m,
            name="relative_velocity_rate_bound_m_per_s",
        ),
        _ceil_div_units(
            raw_relative_velocity_units * time_scale_units_per_second,
            time_step_units,
            name="relative_velocity_rate_bound_units_per_second",
        ),
    )
    residual_rate_units = max(
        _nonnegative_units(
            residual_bound_m / time_step_s,
            scale=scale_m,
            name="coupling_residual_rate_bound_m_per_s",
        ),
        _ceil_div_units(
            raw_residual_units * time_scale_units_per_second,
            time_step_units,
            name="coupling_residual_rate_bound_units_per_second",
        ),
    )
    relative_velocity_units = _ceil_div_units(
        relative_velocity_rate_units * time_step_units,
        time_scale_units_per_second,
        name="relative_velocity_step_bound_units",
    )
    residual_units = _ceil_div_units(
        residual_rate_units * time_step_units,
        time_scale_units_per_second,
        name="coupling_residual_step_bound_units",
    )
    drive_units = relative_velocity_units + residual_units
    initial_units = _nonnegative_units(
        verified_record.max_spatial_dispersion_m,
        scale=scale_m,
        name="max_spatial_dispersion_m",
    )
    merge_tolerance_units = _nonnegative_units(
        verified_record.spatial_tol_m,
        scale=scale_m,
        name="spatial_tol_m",
    )
    continuous_drive_rate_units = relative_velocity_rate_units + residual_rate_units
    continuous_horizon_drive_units = _ceil_div_units(
        continuous_drive_rate_units * horizon_time_units,
        time_scale_units_per_second,
        name="continuous_horizon_drive_bound_units",
    )
    continuous_linear_budget_units = initial_units + continuous_horizon_drive_units
    continuous_margin_units = merge_tolerance_units - continuous_linear_budget_units
    continuous_envelope_discharged = continuous_margin_units >= 0
    linear_budget_units = initial_units + horizon_steps * drive_units
    gronwall_trace_units = _gronwall_budget_trace(
        initial_tolerance_units=initial_units,
        lipschitz_step_gain_units=gain_units,
        drive_bound_units=drive_units,
        horizon_steps=horizon_steps,
    )
    gronwall_budget_units = gronwall_trace_units[-1]
    gronwall_budget_margin_units = merge_tolerance_units - gronwall_budget_units
    gronwall_trace_sha256 = _gronwall_budget_trace_sha256(
        trace_units=gronwall_trace_units,
        horizon_steps=horizon_steps,
    )
    window_margin_units = gronwall_budget_margin_units
    phase_tolerance_units = _nonnegative_units(
        verified_record.phase_tol_rad,
        scale=scale_rad,
        name="phase_tol_rad",
    )
    phase_dispersion_units = _nonnegative_units(
        verified_record.max_phase_dispersion_rad,
        scale=scale_rad,
        name="max_phase_dispersion_rad",
    )
    configured_phase_drift_units = _nonnegative_units(
        phase_drift_bound_rad,
        scale=scale_rad,
        name="phase_drift_bound_rad",
    )
    phase_budget_units = phase_dispersion_units + configured_phase_drift_units
    phase_margin_units = phase_tolerance_units - phase_budget_units
    phase_budget_discharged = phase_margin_units >= 0
    acceptance_tolerance_units = _nonnegative_units(
        verified_record.kinematic_summary_replay_tolerance,
        scale=scale_m,
        name="acceptance_kinematic_summary_replay_tolerance",
    )
    acceptance_tolerance_limit_units = _nonnegative_units(
        PHA_C_ACCEPTANCE_KINEMATIC_SUMMARY_REPLAY_TOLERANCE,
        scale=scale_m,
        name="acceptance_kinematic_summary_replay_tolerance_limit",
    )
    acceptance_replay_certificate_discharged = (
        verified_record.kinematic_equations_validated
        and acceptance_tolerance_units <= acceptance_tolerance_limit_units
    )
    acceptance_certificate_discharged = (
        gronwall_budget_margin_units >= 0
        and phase_budget_discharged
        and acceptance_replay_certificate_discharged
    )
    observed_velocity_step_units = _nonnegative_units(
        verified_record.max_abs_velocity_m_per_s * verified_record.dt,
        scale=scale_m,
        name="observed_velocity_step_m",
    )
    path_length_units = _nonnegative_units(
        verified_record.path_length_max_m,
        scale=scale_m,
        name="path_length_max_m",
    )
    discharged = (
        window_margin_units >= 0
        and phase_margin_units >= 0
        and phase_budget_discharged
        and acceptance_certificate_discharged
        and continuous_envelope_discharged
        and verified_record.execution_disabled
        and not verified_record.actuating
        and verified_record.claim_boundary == PHA_C_ACCEPTANCE_CLAIM_BOUNDARY
    )
    payload_without_hash: dict[str, Any] = {
        "schema_version": PHA_C_FORMAL_OBLIGATION_SCHEMA,
        "evidence_kind": PHA_C_FORMAL_OBLIGATION_EVIDENCE_KIND,
        "claim_boundary": PHA_C_FORMAL_OBLIGATION_CLAIM_BOUNDARY,
        "acceptance_claim_boundary": verified_record.claim_boundary,
        "execution_disabled": True,
        "actuating": False,
        "lean_module": PHA_C_FORMAL_LEAN_MODULE,
        "lean_certificate_predicate": PHA_C_FORMAL_CERTIFICATE_PREDICATE,
        "lean_theorem": PHA_C_FORMAL_CERTIFICATE_THEOREM,
        "continuous_lean_module": PHA_C_FORMAL_CONTINUOUS_LEAN_MODULE,
        "continuous_certificate_predicate": (
            PHA_C_FORMAL_CONTINUOUS_CERTIFICATE_PREDICATE
        ),
        "continuous_theorem": PHA_C_FORMAL_CONTINUOUS_CERTIFICATE_THEOREM,
        "phase_lean_module": PHA_C_FORMAL_PHASE_LEAN_MODULE,
        "phase_certificate_predicate": PHA_C_FORMAL_PHASE_CERTIFICATE_PREDICATE,
        "phase_theorem": PHA_C_FORMAL_PHASE_CERTIFICATE_THEOREM,
        "acceptance_certificate_predicate": (
            PHA_C_FORMAL_ACCEPTANCE_CERTIFICATE_PREDICATE
        ),
        "acceptance_certificate_theorem": (PHA_C_FORMAL_ACCEPTANCE_CERTIFICATE_THEOREM),
        "fixed_point_scale_m": scale_m,
        "fixed_point_scale_rad": scale_rad,
        "fixed_point_time_scale_s": time_scale,
        "time_step_s": time_step_s,
        "time_scale_units_per_second": time_scale_units_per_second,
        "time_step_units": time_step_units,
        "horizon_time_units": horizon_time_units,
        "initial_tolerance_units": initial_units,
        "lipschitz_step_gain_units": gain_units,
        "relative_velocity_rate_bound_units_per_second": relative_velocity_rate_units,
        "relative_velocity_step_bound_units": relative_velocity_units,
        "configured_coupling_residual_step_bound_units": configured_residual_units,
        "coupling_residual_rate_bound_units_per_second": residual_rate_units,
        "coupling_residual_step_bound_units": residual_units,
        "continuous_drive_rate_bound_units_per_second": continuous_drive_rate_units,
        "continuous_horizon_drive_bound_units": continuous_horizon_drive_units,
        "continuous_linear_budget_units": continuous_linear_budget_units,
        "continuous_margin_units": continuous_margin_units,
        "drive_bound_units": drive_units,
        "merge_window_tolerance_units": merge_tolerance_units,
        "horizon_steps": horizon_steps,
        "linear_budget_units": linear_budget_units,
        "gronwall_budget_units": gronwall_budget_units,
        "gronwall_budget_margin_units": gronwall_budget_margin_units,
        "gronwall_budget_trace_sha256": gronwall_trace_sha256,
        "window_budget_margin_units": window_margin_units,
        "phase_tolerance_units": phase_tolerance_units,
        "max_phase_dispersion_units": phase_dispersion_units,
        "configured_phase_drift_bound_units": configured_phase_drift_units,
        "phase_budget_units": phase_budget_units,
        "phase_margin_units": phase_margin_units,
        "phase_budget_discharged": phase_budget_discharged,
        "acceptance_kinematic_equations_validated": (
            verified_record.kinematic_equations_validated
        ),
        "acceptance_kinematic_summary_replay_tolerance": (
            verified_record.kinematic_summary_replay_tolerance
        ),
        "acceptance_kinematic_summary_replay_tolerance_units": (
            acceptance_tolerance_units
        ),
        "acceptance_kinematic_summary_replay_tolerance_limit_units": (
            acceptance_tolerance_limit_units
        ),
        "acceptance_replay_certificate_discharged": (
            acceptance_replay_certificate_discharged
        ),
        "acceptance_certificate_discharged": acceptance_certificate_discharged,
        "observed_velocity_step_units": observed_velocity_step_units,
        "kinematic_residual_units": observed_residual_units,
        "path_length_units": path_length_units,
        "max_spatial_dispersion_units": initial_units,
        "continuous_envelope_discharged": continuous_envelope_discharged,
        "proof_obligations_discharged": discharged,
        "acceptance_sha256": verified_record.acceptance_sha256,
        "timeline_sha256": verified_record.timeline_sha256,
    }
    return PHACKinematicProofObligation(
        **payload_without_hash,
        record_sha256=_sha256_json(payload_without_hash),
    )

pha_c_kinematic_proof_obligation_to_dict ¶

pha_c_kinematic_proof_obligation_to_dict(
    obligation: PHACKinematicProofObligation,
) -> dict[str, bool | float | int | str]

Return a verified canonical JSON-safe proof-obligation manifest.

Parameters¶

obligation : PHACKinematicProofObligation The PHA-C kinematic proof obligation to verify and serialise.

Returns¶

dict[str, bool | float | int | str] The verified canonical JSON-safe proof-obligation manifest.

Source code in src/scpn_phase_orchestrator/upde/pha_c_formal_obligation.py

def pha_c_kinematic_proof_obligation_to_dict(
    obligation: PHACKinematicProofObligation,
) -> dict[str, bool | float | int | str]:
    """Return a verified canonical JSON-safe proof-obligation manifest.

    Parameters
    ----------
    obligation : PHACKinematicProofObligation
        The PHA-C kinematic proof obligation to verify and serialise.

    Returns
    -------
    dict[str, bool | float | int | str]
        The verified canonical JSON-safe proof-obligation manifest.
    """
    verified = verify_pha_c_kinematic_proof_obligation(obligation)
    payload = _dict_without_record_hash(verified)
    payload["record_sha256"] = verified.record_sha256
    return payload

verify_pha_c_kinematic_proof_obligation ¶

verify_pha_c_kinematic_proof_obligation(
    obligation: PHACKinematicProofObligation,
) -> PHACKinematicProofObligation

Validate a PHA-C Lean proof-obligation manifest fail-closed.

Parameters¶

obligation : PHACKinematicProofObligation The PHA-C kinematic proof obligation to operate on.

Returns¶

PHACKinematicProofObligation The same obligation after fail-closed validation.

Raises¶

TypeError If the manifest has the wrong type. ValueError If the manifest fails validation.

Source code in src/scpn_phase_orchestrator/upde/pha_c_formal_obligation.py

def verify_pha_c_kinematic_proof_obligation(
    obligation: PHACKinematicProofObligation,
) -> PHACKinematicProofObligation:
    """Validate a PHA-C Lean proof-obligation manifest fail-closed.

    Parameters
    ----------
    obligation : PHACKinematicProofObligation
        The PHA-C kinematic proof obligation to operate on.

    Returns
    -------
    PHACKinematicProofObligation
        The same obligation after fail-closed validation.

    Raises
    ------
    TypeError
        If the manifest has the wrong type.
    ValueError
        If the manifest fails validation.
    """
    if not isinstance(obligation, PHACKinematicProofObligation):
        raise TypeError("obligation must be a PHACKinematicProofObligation")
    exact_strings = {
        "schema_version": PHA_C_FORMAL_OBLIGATION_SCHEMA,
        "evidence_kind": PHA_C_FORMAL_OBLIGATION_EVIDENCE_KIND,
        "claim_boundary": PHA_C_FORMAL_OBLIGATION_CLAIM_BOUNDARY,
        "acceptance_claim_boundary": PHA_C_ACCEPTANCE_CLAIM_BOUNDARY,
        "lean_module": PHA_C_FORMAL_LEAN_MODULE,
        "lean_certificate_predicate": PHA_C_FORMAL_CERTIFICATE_PREDICATE,
        "lean_theorem": PHA_C_FORMAL_CERTIFICATE_THEOREM,
        "continuous_lean_module": PHA_C_FORMAL_CONTINUOUS_LEAN_MODULE,
        "continuous_certificate_predicate": (
            PHA_C_FORMAL_CONTINUOUS_CERTIFICATE_PREDICATE
        ),
        "continuous_theorem": PHA_C_FORMAL_CONTINUOUS_CERTIFICATE_THEOREM,
        "phase_lean_module": PHA_C_FORMAL_PHASE_LEAN_MODULE,
        "phase_certificate_predicate": PHA_C_FORMAL_PHASE_CERTIFICATE_PREDICATE,
        "phase_theorem": PHA_C_FORMAL_PHASE_CERTIFICATE_THEOREM,
        "acceptance_certificate_predicate": (
            PHA_C_FORMAL_ACCEPTANCE_CERTIFICATE_PREDICATE
        ),
        "acceptance_certificate_theorem": (PHA_C_FORMAL_ACCEPTANCE_CERTIFICATE_THEOREM),
    }
    for field, expected in exact_strings.items():
        got = getattr(obligation, field)
        if got != expected:
            raise ValueError(f"{field} must be {expected!r}")

    if not _validate_bool(
        obligation.execution_disabled,
        name="execution_disabled",
    ):
        raise ValueError("execution_disabled must be true")
    if _validate_bool(obligation.actuating, name="actuating"):
        raise ValueError("actuating must be false")
    _validate_positive_scale(
        obligation.fixed_point_scale_m,
        name="fixed_point_scale_m",
    )
    _validate_positive_scale(
        obligation.fixed_point_scale_rad,
        name="fixed_point_scale_rad",
    )
    _validate_positive_scale(
        obligation.fixed_point_time_scale_s,
        name="fixed_point_time_scale_s",
    )
    _validate_positive_scale(obligation.time_step_s, name="time_step_s")
    nat_fields = (
        "time_scale_units_per_second",
        "time_step_units",
        "horizon_time_units",
        "initial_tolerance_units",
        "lipschitz_step_gain_units",
        "relative_velocity_rate_bound_units_per_second",
        "relative_velocity_step_bound_units",
        "configured_coupling_residual_step_bound_units",
        "coupling_residual_rate_bound_units_per_second",
        "coupling_residual_step_bound_units",
        "continuous_drive_rate_bound_units_per_second",
        "continuous_horizon_drive_bound_units",
        "continuous_linear_budget_units",
        "drive_bound_units",
        "merge_window_tolerance_units",
        "horizon_steps",
        "linear_budget_units",
        "gronwall_budget_units",
        "phase_tolerance_units",
        "max_phase_dispersion_units",
        "configured_phase_drift_bound_units",
        "phase_budget_units",
        "acceptance_kinematic_summary_replay_tolerance_units",
        "acceptance_kinematic_summary_replay_tolerance_limit_units",
        "observed_velocity_step_units",
        "kinematic_residual_units",
        "path_length_units",
        "max_spatial_dispersion_units",
    )
    for field in nat_fields:
        _validate_int(getattr(obligation, field), name=field, minimum=0)
    _validate_int(
        obligation.gronwall_budget_margin_units,
        name="gronwall_budget_margin_units",
        minimum=-(10**18),
    )
    _validate_int(
        obligation.window_budget_margin_units,
        name="window_budget_margin_units",
        minimum=-(10**18),
    )
    _validate_int(
        obligation.continuous_margin_units,
        name="continuous_margin_units",
        minimum=-(10**18),
    )
    _validate_sha256_hex(
        obligation.gronwall_budget_trace_sha256,
        name="gronwall_budget_trace_sha256",
    )
    _validate_int(
        obligation.phase_margin_units,
        name="phase_margin_units",
        minimum=-(10**18),
    )
    _validate_bool(
        obligation.phase_budget_discharged,
        name="phase_budget_discharged",
    )
    if not _validate_bool(
        obligation.acceptance_kinematic_equations_validated,
        name="acceptance_kinematic_equations_validated",
    ):
        raise ValueError("acceptance_kinematic_equations_validated must be true")
    kinematic_replay_tolerance = _validate_positive_scale(
        obligation.acceptance_kinematic_summary_replay_tolerance,
        name="acceptance_kinematic_summary_replay_tolerance",
    )
    if (
        kinematic_replay_tolerance
        != PHA_C_ACCEPTANCE_KINEMATIC_SUMMARY_REPLAY_TOLERANCE
    ):
        raise ValueError(
            "acceptance_kinematic_summary_replay_tolerance must match "
            "the acceptance constant"
        )
    expected_acceptance_tolerance_units = _nonnegative_units(
        kinematic_replay_tolerance,
        scale=obligation.fixed_point_scale_m,
        name="acceptance_kinematic_summary_replay_tolerance",
    )
    if (
        obligation.acceptance_kinematic_summary_replay_tolerance_units
        != expected_acceptance_tolerance_units
    ):
        raise ValueError(
            "acceptance_kinematic_summary_replay_tolerance_units must replay",
        )
    expected_acceptance_tolerance_limit_units = _nonnegative_units(
        PHA_C_ACCEPTANCE_KINEMATIC_SUMMARY_REPLAY_TOLERANCE,
        scale=obligation.fixed_point_scale_m,
        name="acceptance_kinematic_summary_replay_tolerance_limit",
    )
    if (
        obligation.acceptance_kinematic_summary_replay_tolerance_limit_units
        != expected_acceptance_tolerance_limit_units
    ):
        raise ValueError(
            "acceptance_kinematic_summary_replay_tolerance_limit_units must replay",
        )
    _validate_bool(
        obligation.acceptance_replay_certificate_discharged,
        name="acceptance_replay_certificate_discharged",
    )
    _validate_bool(
        obligation.acceptance_certificate_discharged,
        name="acceptance_certificate_discharged",
    )
    _validate_bool(
        obligation.continuous_envelope_discharged,
        name="continuous_envelope_discharged",
    )
    _validate_bool(
        obligation.proof_obligations_discharged,
        name="proof_obligations_discharged",
    )
    _validate_sha256_hex(obligation.acceptance_sha256, name="acceptance_sha256")
    _validate_sha256_hex(obligation.timeline_sha256, name="timeline_sha256")
    _validate_sha256_hex(obligation.record_sha256, name="record_sha256")

    expected_time_scale_units = _ceil_positive_ratio_units(
        1.0,
        obligation.fixed_point_time_scale_s,
        name="time_scale_units_per_second",
    )
    if obligation.time_scale_units_per_second != expected_time_scale_units:
        raise ValueError("time_scale_units_per_second must match time scale")
    expected_time_step_units = _ceil_positive_ratio_units(
        obligation.time_step_s,
        obligation.fixed_point_time_scale_s,
        name="time_step_units",
    )
    if obligation.time_step_units != expected_time_step_units:
        raise ValueError("time_step_units must match time step")
    expected_horizon_time_units = obligation.horizon_steps * obligation.time_step_units
    if obligation.horizon_time_units != expected_horizon_time_units:
        raise ValueError("horizon_time_units must match horizon and time step")

    expected_relative_velocity_units = _ceil_div_units(
        obligation.relative_velocity_rate_bound_units_per_second
        * obligation.time_step_units,
        obligation.time_scale_units_per_second,
        name="relative_velocity_step_bound_units",
    )
    if (
        obligation.relative_velocity_step_bound_units
        != expected_relative_velocity_units
    ):
        raise ValueError(
            "relative_velocity_step_bound_units must match sampled rate bound",
        )
    expected_residual_units = _ceil_div_units(
        obligation.coupling_residual_rate_bound_units_per_second
        * obligation.time_step_units,
        obligation.time_scale_units_per_second,
        name="coupling_residual_step_bound_units",
    )
    if obligation.coupling_residual_step_bound_units != expected_residual_units:
        raise ValueError(
            "coupling_residual_step_bound_units must match sampled rate bound",
        )

    expected_continuous_drive_rate = (
        obligation.relative_velocity_rate_bound_units_per_second
        + obligation.coupling_residual_rate_bound_units_per_second
    )
    if (
        obligation.continuous_drive_rate_bound_units_per_second
        != expected_continuous_drive_rate
    ):
        raise ValueError(
            "continuous_drive_rate_bound_units_per_second must equal rate sum",
        )
    expected_continuous_horizon_drive = _ceil_div_units(
        expected_continuous_drive_rate * obligation.horizon_time_units,
        obligation.time_scale_units_per_second,
        name="continuous_horizon_drive_bound_units",
    )
    if (
        obligation.continuous_horizon_drive_bound_units
        != expected_continuous_horizon_drive
    ):
        raise ValueError(
            "continuous_horizon_drive_bound_units must match sampled horizon rate",
        )
    expected_continuous_linear_budget = (
        obligation.initial_tolerance_units + expected_continuous_horizon_drive
    )
    if obligation.continuous_linear_budget_units != (expected_continuous_linear_budget):
        raise ValueError(
            "continuous_linear_budget_units must match continuous envelope",
        )
    expected_continuous_margin = (
        obligation.merge_window_tolerance_units - expected_continuous_linear_budget
    )
    if obligation.continuous_margin_units != expected_continuous_margin:
        raise ValueError("continuous_margin_units must match continuous envelope")
    expected_continuous_discharged = expected_continuous_margin >= 0
    if obligation.continuous_envelope_discharged != expected_continuous_discharged:
        raise ValueError(
            "continuous_envelope_discharged does not match certificate math",
        )

    expected_drive = (
        obligation.relative_velocity_step_bound_units
        + obligation.coupling_residual_step_bound_units
    )
    if obligation.drive_bound_units != expected_drive:
        raise ValueError("drive_bound_units must equal relative velocity plus residual")
    if obligation.kinematic_residual_units > (
        obligation.coupling_residual_step_bound_units
    ):
        raise ValueError("kinematic_residual_units must fit sampled residual bound")
    if obligation.configured_coupling_residual_step_bound_units > (
        obligation.coupling_residual_step_bound_units
    ):
        raise ValueError(
            "configured_coupling_residual_step_bound_units must fit residual bound",
        )
    if obligation.max_spatial_dispersion_units != obligation.initial_tolerance_units:
        raise ValueError("max_spatial_dispersion_units must mirror initial tolerance")
    expected_budget = (
        obligation.initial_tolerance_units
        + obligation.horizon_steps * obligation.drive_bound_units
    )
    if obligation.linear_budget_units != expected_budget:
        raise ValueError("linear_budget_units must match the Lean linear budget")
    expected_gronwall_trace = _gronwall_budget_trace(
        initial_tolerance_units=obligation.initial_tolerance_units,
        lipschitz_step_gain_units=obligation.lipschitz_step_gain_units,
        drive_bound_units=obligation.drive_bound_units,
        horizon_steps=obligation.horizon_steps,
    )
    expected_gronwall_budget = expected_gronwall_trace[-1]
    if obligation.gronwall_budget_units != expected_gronwall_budget:
        raise ValueError("gronwall_budget_units must match the Lean Gronwall budget")
    expected_gronwall_margin = (
        obligation.merge_window_tolerance_units - expected_gronwall_budget
    )
    if obligation.gronwall_budget_margin_units != expected_gronwall_margin:
        raise ValueError("gronwall_budget_margin_units must match the Lean margin")
    expected_trace_hash = _gronwall_budget_trace_sha256(
        trace_units=expected_gronwall_trace,
        horizon_steps=obligation.horizon_steps,
    )
    if obligation.gronwall_budget_trace_sha256 != expected_trace_hash:
        raise ValueError("gronwall_budget_trace_sha256 does not replay")
    expected_margin = expected_gronwall_margin
    if obligation.window_budget_margin_units != expected_margin:
        raise ValueError("window_budget_margin_units must match the Lean margin")
    expected_phase_budget = (
        obligation.max_phase_dispersion_units
        + obligation.configured_phase_drift_bound_units
    )
    if obligation.phase_budget_units != expected_phase_budget:
        raise ValueError(
            "phase_budget_units must match dispersion plus configured drift",
        )
    expected_phase_margin = obligation.phase_tolerance_units - expected_phase_budget
    if obligation.phase_margin_units != expected_phase_margin:
        raise ValueError(
            "phase_margin_units must match phase tolerance minus phase budget",
        )
    expected_phase_budget_discharged = expected_phase_margin >= 0
    if obligation.phase_budget_discharged != expected_phase_budget_discharged:
        raise ValueError(
            "phase_budget_discharged does not match phase certificate math",
        )
    expected_acceptance_replay_discharged = (
        obligation.acceptance_kinematic_equations_validated
        and obligation.acceptance_kinematic_summary_replay_tolerance_units
        <= obligation.acceptance_kinematic_summary_replay_tolerance_limit_units
    )
    if (
        obligation.acceptance_replay_certificate_discharged
        != expected_acceptance_replay_discharged
    ):
        raise ValueError(
            "acceptance_replay_certificate_discharged does not match Lean replay",
        )
    expected_acceptance_certificate_discharged = (
        expected_margin >= 0
        and expected_phase_budget_discharged
        and expected_acceptance_replay_discharged
    )
    if (
        obligation.acceptance_certificate_discharged
        != expected_acceptance_certificate_discharged
    ):
        raise ValueError(
            "acceptance_certificate_discharged does not match Lean certificate",
        )
    expected_discharged = (
        expected_margin >= 0
        and expected_phase_budget_discharged
        and expected_acceptance_certificate_discharged
        and expected_continuous_discharged
        and obligation.execution_disabled
        and not obligation.actuating
    )
    if obligation.proof_obligations_discharged != expected_discharged:
        raise ValueError("proof_obligations_discharged does not match certificate math")
    expected_hash = _sha256_json(_dict_without_record_hash(obligation))
    if obligation.record_sha256 != expected_hash:
        raise ValueError("record_sha256 does not match canonical obligation payload")
    return obligation

UPDE — PHA-C Lean Kinematic Proof Obligation¶

Formal guarantee boundary¶

Use cases¶

Fixed-point mapping¶

Minimal example¶

Verification boundary¶

PHACKinematicProofObligation dataclass ¶

Methods:¶

to_dict ¶

Returns¶

build_pha_c_kinematic_proof_obligation ¶

Parameters¶

Returns¶

pha_c_kinematic_proof_obligation_to_dict ¶

Parameters¶

Returns¶

verify_pha_c_kinematic_proof_obligation ¶

Parameters¶

Returns¶

Raises¶

PHACKinematicProofObligation `dataclass` ¶