Skip to content

fix: align B.3 G-composition with USM path semantics #34

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
iqdoctor wants to merge 1 commit into
base: main
Choose a base branch
from
+8 −6
Open

fix: align B.3 G-composition with USM path semantics #34

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 8 additions & 6 deletions FPF-Spec.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26244,12 +26244,14 @@ Any Γ‑flavour that claims an **Assurance** result **must** adopt the followin
2. **ClaimScope:**

```
G_eff = SpanUnion({G_i}) constrained by support
G_path(P) = ⋂_{i ∈ P} G_i
G_eff = SpanUnion({G_path(P)}) constrained by support and declared independence
```

* “SpanUnion” is a **set/coverage union** in the domain’s space.
* **Constraint:** any region in the union **unsupported** by reliable parts is **dropped** (WLNK).
* *Monotone:* adding supported span cannot reduce `G_eff`.
* On an **essential dependency path**, scope composes by **intersection**.
* `SpanUnion` is used only across **independent support lines to the same claim**.
* **Constraint:** any region in the union **unsupported** by reliable independent lines is **dropped** (WLNK).
* *Monotone:* adding supported independent span cannot reduce `G_eff`.

3. **Reliability (penalized by integration):**

Expand Down Expand Up @@ -26439,10 +26441,10 @@ These obligations refine the generic Proof Kit from **B.1.1 §6** for **assuranc
| ID | Requirement | Purpose | |
| ----------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------------------------------------------- | --------------------------------- |
| **CC‑B3.1** | An assurance result **SHALL** be a typed claim \`Assurance(H, C | K, S)`with`S ∈ {design, run}\`. | Prevent scope drift and chimeras. |
| **CC‑B3.2** | `F` **SHALL** be treated as **ordinal** (`min`/thresholds only); `G` as **coverage** (set/measure union constrained by support); `R` as **ratio** (`min` + conservative ops). | Preserve scale integrity (CHR). | |
| **CC‑B3.2** | `F` **SHALL** be treated as **ordinal** (`min`/thresholds only); `G` as a **USM scope object** (path intersection plus independent-line `SpanUnion`); `R` as **ratio** (`min` + conservative ops). | Preserve scale integrity (CHR). | |
| **CC‑B3.3** | The **Congruence Level** `CL` **SHALL** live on **edges**; the penalty `Φ(CL)` **SHALL** be **monotone decreasing** and **bounded** (`R_eff ≥ 0`). | Make integration quality first‑class. | |
| **CC‑B3.4** | `R_eff` **SHALL** be computed as `R_eff = max(0, min_i R_i − Φ(CL_min))` for the relevant integration path(s), unless a stricter domain‑specific rule is justified. | Enforce WLNK and penalize weak integrations. | |
| **CC‑B3.5** | `F_eff = min_i F_i`; `G_eff = SpanUnion({G_i})` **constrained by support**. | Prevent over‑generalization. | |
| **CC‑B3.5** | `F_eff = min_i F_i`; for `G`, essential dependency paths **SHALL** compose by **intersection**, and `G_eff` **MAY** use `SpanUnion` only across **declared independent support lines** to the same claim. | Prevent over‑generalization. | |
| **CC‑B3.6** | An **Assurance SCR** **SHALL** be produced, listing node/edge values, Evidence Graph Ref, and any OrderSpec/TimeWindow identifiers, **and SHALL also display**: (i) the **describedEntity binding** `describe(Object→GroundingHolon)` for the claim and the declared **CHR:ReferencePlane ∈ {world|concept|episteme}** (cf. C.2.3); (ii) a **TA/VA/LA breakdown** of anchored evidence **kept separable** per **CC–KD‑08**, with **decay/valid‑until** indicators on empirical bindings (A.10), and the **Epistemic‑Debt** tally as computed in **§ B.3.4**. | Provide auditability (A.10). |
| **CC‑B3.7** | **Agency‑CHR** values (A.13) **SHALL NOT** override WLNK or `Φ(CL)` penalties; if agency grade change alters capabilities, model it as a **Meta‑Holon Transition**. | Preserve safety; keep agency separate. | |
| **CC‑B3.8** | Design‑time and run‑time assurance **SHALL NOT** be mixed in one tuple; compare them side‑by‑side if needed. | Avoid design/run mixing. | |
Expand Down