permits_append
plain-language theorem explainer
The lemma establishes that consent permission for a ledger whose windows are the concatenation of two lists equals the disjunction of the permissions from each list separately. Modelers composing temporal consent records in recognition systems cite it to simplify ledger checks. The proof is a tactic script that unfolds the permits predicate and reduces via the standard list-append distributivity law.
Claim. For any type $A$, lists $L_1,L_2$ of consent windows over $A$, time $t$, and action $a$, the permission predicate on the ledger with windows $L_1++L_2$ at $(t,a)$ holds if and only if the permission predicate on the ledger with windows $L_1$ or the one with windows $L_2$ holds at $(t,a)$.
background
ConsentWindow is a structure carrying an action scope predicate, start time, optional end time, and optional revocation time. ConsentLedger packages a list of such windows. The permits operation on a ledger returns true precisely when List.any of the windows satisfies the per-window permitsAt predicate at the given time and action.
proof idea
The proof is a tactic-mode script. It unfolds ConsentLedger.permits, then invokes simp with the List.any_append lemma to replace the existential check over the concatenated list by the disjunction of the two separate checks.
why it matters
The lemma supplies a basic algebraic identity for consent-ledger composition inside the Recognition.Consent module. It supports downstream reasoning about temporal permissions that may feed into actualization operators and forcing-chain constructions, although no direct used-by edges are recorded. It mirrors the clean reduction properties seen in the J-cost and phi-ladder identities elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.