revoke_narrows_active
plain-language theorem explainer
Revocation at time r on a consent window narrows its active interval such that activity after revocation at t implies the window was already active at t beforehand. Modal actualization researchers in Recognition Science cite this when composing consent ledgers. The proof is a direct term-mode case split on the optional termination time followed by boolean simplification.
Claim. Let $w$ be a consent window over actions of type $A$, and let $r,t$ be natural numbers. If the window remains active at time $t$ after revocation is applied at $r$, then the original window is active at $t$.
background
ConsentWindow is a structure with a scope predicate over actions $A$, a start time tStart, optional end time tEnd?, and optional revocation time revokedAt?. The predicate activeAt holds at time $t$ precisely when tStart ≤ t, $t$ lies before any recorded end time, and $t$ precedes any recorded revocation time. revokeAt updates the revocation field to the minimum of any prior revocation and the new time $r$ (or sets it to $r$ if none existed). This lemma belongs to the Consent module, which supplies time-bounded permission tracking for the modal actualization operator A that selects realized configurations from possibilities.
proof idea
The proof unfolds activeAt and revokeAt, introduces the hypothesis, then applies by_cases on whether w.tEnd? equals none. Each branch performs cases on the option value and finishes with simp on the resulting boolean expressions.
why it matters
The lemma is invoked by revoke_narrows_perm to extend the narrowing property from activeAt to the full permitsAt predicate. It supplies a basic monotonicity fact inside the consent ledger construction, supporting permission narrowing steps that align with the Recognition Composition Law and the eight-tick octave structure. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.