FPF Reference

C.3.A:B.9 End‑to‑end example (manager’s cheat‑sheet) [I]

Preface node heading:c-3-a-b-9-end-to-end-example-manager-s-cheat-sheet-i:34423

Content

Scenario. You want to publish “∀ x: PassengerCar. brakeDistance ≤ 50 m dry; ≤ 40 m wet” across two plants.

  1. Kinds. PassengerCar ⊑ Vehicle (K2, signature F4).
  2. Scope (G). {surface in {dry, wet}, speed limits, rig version, time selector (Γ_time)=rolling 180 days} in Plant‑A.
  3. VA. Prove the property for PassengerCar using a proof assistant, and cite the Scope slices it assumes.
  4. LA. Build an evidence matrix with rows {PassengerCar} and columns {dry, up to 50} and {wet, up to 40}, including rig variants; add boundary tests near the limits.
  5. TA. Qualify the prover kernel and the automated checker used for wet surrogates.
  6. Bridge. To Plant‑B: a Scope Bridge with CL=2 (rig bias) and a KindBridge with CL^k=3 (same classification).
  7. Penalties. Apply the scope‑bridge penalty for CL=2 and the kind‑bridge penalty for CL^k=3 to R. Per policy, add extra test cells in Plant‑B to compensate for rig bias.
  8. Guards. Use Guard_EvidenceAttach_Typed on the state change; include freshness checks.

Outcome. A defensible, auditable publication: typed, scoped, with clear evidence coverage and explicit risk penalties — no conflation of abstraction with applicability, and no tool risk smuggled into content.