Module require 

Turning an undecided answer into a refusal.

The lattice reports three values; the compiler acts on two. This module is the boundary, and it collapses Tri::Unknown into an error every time.

There is no permissive mode

Deliberately, there is no flag, feature, or alternate entry point that lets an Unknown through as a pass. That is Goal G5 — if a property cannot be proved, reject or degrade, never assume — and it only holds if there is no escape hatch. An escape hatch would be used, and it would be used on the day someone is in a hurry.

The cost of that strictness is a build error on a pattern the solver cannot decide. The cost of the alternative is a permission granted on a guess. The two are not comparable, so the strict reading wins.

Every refusal names the offending pair and says why, so the fix is obvious: narrow a grant, spell a pattern inside the decidable fragment, or degrade a par to a seq.

Enums

Refusal

Why the solver refused a flow.

Functions

require_attenuated

Require that child is within parent — the Law I attenuation check.

require_disjoint

Require that two branches cannot interfere — the par proof.