permitsAt
plain-language theorem explainer
The definition permitsAt returns true for an action a at time t under consent window w exactly when the window is temporally active and a lies in its scope. Consent modelers in recognition frameworks cite it when composing permission predicates over ledgers or revocation rules. It is realized as a direct boolean conjunction of the activeAt temporal test and the window scope predicate.
Claim. Let $w$ be a consent window over actions of type $A$, let $t$ be a natural number, and let $a$ belong to $A$. Then permitsAt$(w,t,a)$ holds if and only if $w$ is active at $t$ and the scope predicate of $w$ returns true on $a$.
background
A consent window is a record containing a scope map from actions to booleans, a start tick tStart, an optional end tick, and an optional revocation tick. The companion activeAt predicate verifies that the current tick meets or exceeds the start, respects any end bound, and precedes any revocation time. The present definition lives inside the Recognition.Consent module, which supplies permission primitives for recognition processes.
proof idea
One-line definition that returns the conjunction of activeAt w t and w.scope a. It invokes the sibling activeAt predicate and projects the scope field from the ConsentWindow record.
why it matters
The definition is invoked by the permits aggregator over a ConsentLedger and by the revoke_narrows_perm lemma that shows revocation preserves the implication direction. It supplies the atomic permission test inside the consent layer of the Recognition framework, sitting downstream of the actualization operator A that selects realized configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.