E.4.PFR:4.5 - Establishment, minimality and a total answer
For a receiving derivation of p under ordinary premise introduction, both {p} and {p,q} are sufficient without any undeclared premise. Both can be established when their required axes are true; only {p} is inclusion-minimal among their sub-bases. If the receiver requires a minimal family and that additional search is incomplete, the minimal-family answer stays qualified while establishment of these two bases survives.
| Bounded cell case | Exactly one disposition and retained distinction |
|---|---|
| Closed universe {{p},{p,q}}, required axes true, both yield p and their required pair is compatible | established-compatible; optional minimality can remain unknown without changing that result. |
| Closed universe with one otherwise sufficient candidate and an unknown witness required by this receiver | open-no-established; the missing witness leaves the conjunction unresolved. |
| Closed universe with one candidate whose exactness is false and required witness unknown | closed-insufficient; false exactness decisively defeats it. |
| One established candidate in an open universe | established-with-open-candidates; retain the candidate while admitting further alternatives may matter. |
| Two independently sufficient, established bases with known incompatible consequences for the same overlapping use | established-conflict, even if another candidate is unresolved; neither established basis is deleted. |
| Closed empty universe and an exact supported absent-needed-content claim | missing-candidates. |
| Closed empty universe with no supported claim that content is needed | closed-empty-unresolved-need. |
In evaluate mode, criterion “value ≥ 80” and an applicable exact value 70 suffice to obtain fail under that evaluation rule. With the other required axes true, the candidate is established even though the evaluated object fails. The criterion/value set’s sufficiency says nothing about whether a particular evaluation actually selected and used it; Lane 3’s actual-use predicates still need their own facts.