ConsentLedger
plain-language theorem explainer
ConsentLedger aggregates a list of time-bounded consent windows over an action type A. Researchers modeling permission systems inside Recognition Science cite this record when composing consent states for actualization steps. The declaration is a plain structure definition with one field and no computational content.
Claim. Let $A$ be a type of actions. A consent ledger over $A$ is a record whose single field holds a finite list of consent windows; each window pairs a scope predicate $A → Bool$, a start time in natural numbers, an optional end time, and an optional revocation time.
background
The Recognition.Consent module models permissions via ConsentWindow records. Each such window carries a scope function that selects permitted actions, together with temporal bounds given by a start tick and optional end or revocation markers. The local setting places consent inside modal actualization, where lists of windows determine which configurations can be realized at a given tick.
proof idea
Structure definition that introduces the record type with a single field for the list of windows. No lemmas or tactics are invoked; the declaration serves only as a type constructor for the downstream permits function and its append lemma.
why it matters
This record supplies the data type used by the permits predicate and the permits_append lemma inside the same module. It thereby supports composition of consent states, which is a prerequisite for tracking permissions during actualization. The structure remains independent of the core forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.