permits_append
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove properties of revocation times or overlapping windows.
- Does not extend the identity to non-list ledger representations.
- Does not address empty-list edge cases beyond the general append law.
- Does not connect the permission predicate to the A operator or mass formulas.
formal statement (Lean)
63@[simp] lemma permits_append {A} (L1 L2 : List (ConsentWindow A)) (t : Nat) (a : A) :
64 (ConsentLedger.permits { windows := L1 ++ L2 } t a)
proof body
Tactic-mode proof.
65 = (ConsentLedger.permits { windows := L1 } t a
66 || ConsentLedger.permits { windows := L2 } t a) := by
67 unfold ConsentLedger.permits
68 simp [List.any_append]
69
70end ConsentLedger
71
72end Recognition
73end IndisputableMonolith
74