revokeAt
revokeAt takes a ConsentWindow over actions A and a time r, returning an updated window whose revocation timestamp is the minimum of r and any prior revocation. Consent modelers in Recognition Science cite it when showing revocation only restricts permissions. The definition performs a direct record update that applies a min operation to the optional revokedAt? field.
claimGiven a consent window $w$ over actions of type $A$ and revocation time $r$, the updated window has the same scope, $tStart$, and $tEnd?$ as $w$, but its revocation time is set to $r$ if none existed or to the minimum of $r$ and the prior revocation time.
background
ConsentWindow is the structure with fields scope : A → Bool, tStart : Nat, optional tEnd? : Option Nat, and optional revokedAt? : Option Nat. It records time-bounded consent constraints in the Recognition.Consent module. The definition depends on the ConsentWindow structure itself and on Nat operations for the min update. Related upstream notions include the active edge count A from IntegrationGap and Actualization, though they supply only notational context here.
proof idea
The definition is a one-line record update that replaces revokedAt? with some value. It matches on the existing revokedAt? and applies Nat.min to the supplied r when a prior revocation exists, otherwise uses r directly.
why it matters in Recognition Science
revokeAt supplies the revocation operator used by the downstream lemmas revoke_narrows_active and revoke_narrows_perm, which prove that revocation narrows active and permitted actions. It implements the constraint-narrowing step inside the Recognition consent model, consistent with the framework's treatment of time-bounded permissions. No open scaffolding questions are closed by this definition.
scope and limits
- Does not change the scope predicate or tStart of the window.
- Does not modify the optional end time tEnd?.
- Does not enforce that r lies after tStart.
- Does not interact with the actualization operator A or mass formulas.
formal statement (Lean)
24def revokeAt {A} (w : ConsentWindow A) (r : Nat) : ConsentWindow A :=
proof body
Definition body.
25 { w with revokedAt? := some (match w.revokedAt? with | none => r | some tr => Nat.min tr r) }
26