revoke_narrows_perm
plain-language theorem explainer
Revocation of a consent window at time r narrows the set of permitted actions at evaluation time t without adding permissions. Researchers formalizing permission systems or consent ledgers within Recognition Science cite this for its monotonicity property. The tactic proof unfolds permitsAt, reduces the active-time component via the sibling active-narrowing lemma, and resolves the scope predicate by boolean case analysis and simplification.
Claim. Let $w$ be a consent window over actions of type $A$, with revocation time $r$, evaluation time $t$, and action $a$. If $a$ is permitted at $t$ in the window obtained by revoking $w$ at $r$, then $a$ is permitted at $t$ in the original window $w$.
background
ConsentWindow is a structure over actions $A$ consisting of a scope predicate $A$ to Bool, a start time, an optional end time, and an optional revocation time. This encodes time-bounded permissions that support revocation in the Recognition framework. The module Consent defines windows together with ledgers for tracking permissions over time, drawing on upstream structures such as LedgerFactorization for J-cost calibration and SpectralEmergence for discrete state emergence. The local proof depends on the sibling active-narrowing result for the time component of permissions.
proof idea
The tactic proof unfolds permitsAt, introduces the hypothesis, and obtains the active-time narrowing from revoke_narrows_active applied to the left conjunct of the hypothesis. It then performs case analysis on the boolean value of scope a. The true case simplifies the permitsAt conjunction and rebuilds it using the active result together with reflexivity; the false case simplifies directly to a contradiction.
why it matters
The lemma supplies the monotonicity property required for revocation inside consent windows, supporting ledger construction and operations such as permits_append. It aligns with the ledger factorization and integration-gap structures from upstream results, ensuring conservative updates in the Recognition Science permission model. No open questions are addressed; the result closes a basic consistency property for the consent ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.