ConsentLedger
ConsentLedger aggregates consent windows into a ledger over an action type A. Researchers modeling time-dependent permissions in Recognition Science cite it when composing actualization rules. The structure is a direct record definition with a single field holding the list of windows.
claimA consent ledger over actions of type $A$ consists of a list of consent windows, where each window is a record containing a scope predicate $A → Bool$, a start time $ℕ$, and optional end and revocation times.
background
The Recognition.Consent module models consent through time-bounded structures. ConsentWindow is the base record with fields scope : A → Bool, tStart : Nat, tEnd? : Option Nat, and revokedAt? : Option Nat. ConsentLedger simply packages a list of such windows. The module imports Mathlib and depends on action-type definitions from IntegrationGap, Masses.Anchor, and Modal.Actualization.
proof idea
The declaration is a structure definition that directly introduces the record constructor with the windows field.
why it matters in Recognition Science
ConsentLedger supplies the data type for the permits function, which checks action permission at a tick via any window, and for the permits_append lemma that distributes over list concatenation. It supplies the consent bookkeeping layer inside the Recognition framework's actualization operator A.
scope and limits
- Does not define constructors or validators for individual windows.
- Does not enforce consistency among overlapping time intervals.
- Does not relate windows to J-cost, phi-ladder, or spatial dimension D=3.
- Does not specify revocation semantics beyond the optional field.
formal statement (Lean)
55structure ConsentLedger (A : Type u) where
56 windows : List (ConsentWindow A)
57
58namespace ConsentLedger
59