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

Link to current text

Published source confirmed at last check

Source changed 2026-10-03 11:52:20 UTC · snapshot created 2026-10-03 11:53:41 UTC · last check 2026-10-03 14:05:05 UTC

A.20:4.3 - Constraint families and outcome rules

The following families are recognition aids, not a universal required list. Each application still names the actual constraint, edition, assumptions, case facts, and test.

Constraint familyTriggersatisfied meansOther outcomes
Type, domain, and rangeThe subject consumes or produces typed values.Every case input and result used by the claim lies in the declared type, domain, and range.A counterexample is violated; unavailable values are unknown; a failed test is error.
Admissibility conditionsThe operation or transformation declares guards or admissible cases.Every required guard is true for the case and window.A false guard is violated; undetermined guard truth is unknown.
Law or invariant setThe current claim relies on a named law or invariant.The named invariant holds for the case under its assumptions.A counterexample is violated; missing case facts or witness content are unknown.
Quantity and unit coherenceThe current operation combines quantities or units.The case is coherent under the already declared quantity, unit, and reference-scheme rules.A mismatch is violated; an unrecovered declaration is unknown. A.20 does not define or translate units or planes.
Sensitivity or stability boundA robustness, continuity, perturbation, safety-envelope, or stability claim actually depends on a bound.The cited bound covers the stated domain, assumptions, distance or norm, and case.A counterexample is violated; absent assumptions or certificate content are unknown. No bound is required without this trigger.
Return-shape preservationA consumer relies on a declared set, archive, order, or other non-scalar result shape.The transformation preserves that declared shape for the current case.Hidden scalarization or lost required structure is violated; unrecovered shape facts are unknown. A.20 does not rank or select the result.
A.6.4 retargeting invariantThe exact proposition in q is the named internal constraint for the current use; q remains the C.2.1 bounded-use assertion about r.Exact current case facts establish the proposition as stated, including its invariant, visible loss, named receiving use, conditions, and polarity.A counterexample is violated; a missing deciding fact is unknown unless the constraint itself makes absence a failure. This A.20 result may enter the case basis for A.6.4’s separate satisfies, fails, or cannot decide judgement; it is not that judgement, and the exact current facts remain separately named. r and any application remain separate.

The constraint’s own pattern supplies its truth condition. A.20 supplies the application result form and summary only.