ConsentWindow
ConsentWindow defines a time-bounded consent structure over an action type A, consisting of a scope predicate, start time, optional end time, and optional revocation time. Modelers of permission systems in Recognition Science cite it when tracking active consents across discrete ticks. The declaration is a direct structure definition with default values for the optional fields.
claimA consent window over actions of type $A$ is a structure with a scope predicate $scope: A → {0,1}$, a start time $t_{Start} ∈ ℕ$, an optional end time $t_{End} ∈ ℕ ∪ {none}$, and an optional revocation time $r ∈ ℕ ∪ {none}$.
background
In the Recognition.Consent module, consent is tracked via time windows that gate actions of type A. The structure supplies the minimal fields needed for interval checks and revocation. Upstream, the actualization operator A from Modal.Actualization maps a configuration to the J-cost minimizer among its possibilities, while the constant A from IntegrationGap and Masses.Anchor equals 1 and encodes the active-edge count per tick under the φ-balance at D=3.
proof idea
This is a structure definition. It directly declares the four fields scope, tStart, tEnd?, and revokedAt? with the stated defaults; no lemmas or tactics are invoked.
why it matters in Recognition Science
ConsentWindow is the base type for all downstream consent operations in the module. It is used by activeAt to test activity at a given tick, by permitsAt to combine activity with scope, and by ConsentLedger to hold lists of windows. The structure supplies the temporal scaffolding required for permission checks inside actualization steps of the Recognition framework.
scope and limits
- Does not impose any algebraic relation on the scope predicate.
- Does not resolve conflicts among overlapping windows.
- Does not tie the Nat time fields to the φ-ladder or J-cost.
- Does not define merging or revocation propagation rules.
formal statement (Lean)
9structure ConsentWindow (A : Type u) where
10 scope : A → Bool
11 tStart : Nat
12 tEnd? : Option Nat := none
proof body
Definition body.
13 revokedAt? : Option Nat := none
14
15namespace ConsentWindow
16