fpf.tools
Library / First Principles Framework (FPF) - Core Conceptual Specification
Jump to passage
In this reading
Source · lines 37297–37316

Link to current text

Published source confirmed at last check

Source changed 2026-10-03 05:29:54 UTC · snapshot created 2026-10-03 05:30:57 UTC · last check 2026-10-03 07:05:20 UTC

A.20:7 - Check the ordinary local result

For an ordinary A.20 use, check only these five points:

  1. Subject and constraint (CC-A20-1). Name the exact subject and the exact constraint and edition being applied.
  2. Case and applicability (CC-A20-2). State the assumptions, case facts, scope, evaluation window, and why the constraint is required, optional, or notApplicable.
  3. Evaluation and outcome (CC-A20-2). Record evaluated or notRun. For an evaluated applicable constraint, record satisfied, violated, unknown, or error under the constraint’s own outcome rule.
  4. Support (CC-A20-1). Give the witness, counterexample, missing-information reason, or error reason that supports that result.
  5. Complete summary (CC-A20-3). Use ConstraintValiditySummary=satisfied only when every constraint in the complete declared required set was evaluated and satisfied.

A specialist constraint such as a stability bound, return-shape condition, or retargeting invariant is present only when its trigger in section 4.3 applies (CC-A20-4).

A.20:7.1 - Extensions only when another use is current

TriggerAdditional checkDirect pattern
A gate consumes the resultKeep every applicable GateFit result independently recoverable; an A.20 failure changes only the A.21 aggregate under its current rule (CC-A20-5). A deferred required check remains notRun (CC-A20-6).A.21
The exact proposition in an A.6.4 bounded-use assertion q is the named internal constraintApply A.20 to that proposition for the stated case and return only its ConstraintValidityResult; keep r, q, any operation application, and the A.6.4 current-case judgement separate. A Bridge or reversibility claim enters only when separately current (CC-A20-8).A.6.4; add F.9 only for a separate semantic-correspondence claim
Publication, structure, time, refresh, evidence, assurance, or Work is currentKeep those claims in their own result or relation and follow the direct pattern (CC-A20-9). A.20 adds no publication-face, path, slice, scheduler, gate-profile, or gate-algebra fields (CC-A20-7).E.17, E.18, C.27, G.11, A.10, B.3, or A.15, as applicable