FPF Reference

B.3:5 Proof obligations (attach these when producing an Assurance tuple)

Preface node heading:b-3-5-proof-obligations-attach-these-when-producing-an-assurance-tuple:27152

Content

These obligations refine the generic Proof Kit from B.1.1 §6 for assurance outputs. Each Γ‑flavour that emits an Assurance(H, C | K, S) tuple MUST attach the applicable obligations below.

Common obligations (all Γ‑flavours)

  • ASS‑CLM (Typed claim & context). State the claim C (what is being assured), the context K (assumptions, environment), and the scope S ∈ {design, run}.

  • ASS‑SCA (Scale discipline). Declare the scale kind used for each characteristic (F ordinal, G coverage, R ratio) and confirm that all operations are admissible for that kind (no averaging of ordinals; G via set/coverage ops).

  • ASS‑WLNK (Weakest‑link evidence). Identify the cutset (node or edge set) that caps F/G/R for the claim (the proof spine for epistemes, the structural or assurance bottleneck for systems).

  • ASS‑CL (Congruence path). Identify the relevant integration path(s) and record CL_min used in the penalty Φ(CL_min).

  • ASS‑MAN (SCR). Produce a SCR listing all contributing nodes and edges with (F, G, R) and CL values, their DesignRunTag, and Evidence Graph Ref (A.10). If order or time were material, include the OrderSpec or TimeWindow identifiers from B.1.4.

  • ASS‑MONO (Declared monotone characteristics). List the characteristics along which local improvement cannot reduce the aggregate (this supports future evolution, B.4).

Γ_sys (systems) — additional obligations

  • CORE‑BIC (Interface congruence). Reference the Boundary‑Inheritance Standard (BIC) from B.1.2 and record any interface mismatches; these contribute to CL_min.

  • CORE‑ENV (Operating envelope). Specify the domain used for G (e.g., load–temperature region) and how coverage is computed (set union constrained by support).

Γ_epist (epistemes) — additional obligations

  • EPI‑SPN (Entailment spine). Identify the premise/lemma spine for the claim; R_raw = min R_i is taken along this spine, not over arbitrary satellites.

  • EPI‑MAP (Semantic mapping congruence). Point to the vocabulary/ontology mappings used; their verification status sets the CL levels on the integration edges.

Γ\ctx / Γ\method (order‑sensitive) — additional obligations

  • CTX‑ORD (OrderSpec). Attach the partial or total order σ and any join‑soundness conditions (types, pre/post‑conditions). (See B.1.4 for NC‑1..3 invariants; B.1.5 adds duration/capability typing.)

Γ_time (temporal) — additional obligations

  • TIME‑COV (Coverage & identity). Show that PhaseOf intervals cover the declared window without overlap for the same carrier; justify any gap/overlap explicitly.

Note on Γ_work. Resource spending and efficiency live in Γ_work. Their measurement integrity can influence R for a claim (e.g., if a reliability figure depends on calibrated energy input), but costs themselves are not assurance; keep them in Γ_work and cite their measurement assurance as inputs here.