activeAt
activeAt determines whether a consent window over actions of type A remains active at a given natural-number time t. It would be cited in proofs of temporal permission and revocation narrowing within the Recognition.Consent module. The definition is a direct boolean conjunction checking the window's start bound, optional end bound, and optional revocation bound.
claimFor a consent window $w$ with fields $tStart$, $tEnd?$, and $revokedAt?$, the predicate $activeAt(w,t)$ holds precisely when $tStart ≤ t$, $t ≤ tEnd?$ whenever the optional end is present, and $t < revokedAt?$ whenever the optional revocation is present.
background
ConsentWindow is the structure that packages a scope predicate on actions of type A together with a start time in naturals and optional end and revocation times. The activeAt definition lives inside the Recognition.Consent module, which supplies the temporal layer for consent tracking in the Recognition framework. It depends on the ConsentWindow structure itself and on the various A definitions imported from IntegrationGap, Masses.Anchor, and Modal.Actualization, which supply the active-edge and actualization context used elsewhere in the monolith.
proof idea
This is a definition that expands directly to the conjunction of three boolean conditions on the fields of ConsentWindow: the start-time inequality, the optional end-time check, and the optional revocation-time check. No lemmas are applied; the body is the explicit match-and-compare expression.
why it matters in Recognition Science
activeAt is the primitive used by permitsAt to combine activity with the scope predicate and by revoke_narrows_active to prove that revocation strictly narrows the active interval. It therefore supplies the temporal guard for the consent ledger and sits downstream of the actualization operator A from Modal.Actualization. The definition closes a small but necessary interface in the Recognition consent model without introducing new hypotheses.
scope and limits
- Does not evaluate the scope predicate on actions.
- Does not interpret time beyond the natural numbers.
- Does not propagate revocation effects backward in time.
- Does not constrain the relation between tEnd? and revokedAt?.
formal statement (Lean)
17def activeAt {A} (w : ConsentWindow A) (t : Nat) : Bool :=
proof body
Definition body.
18 (w.tStart ≤ t) && (match w.tEnd? with | none => True | some te => t ≤ te)
19 && (match w.revokedAt? with | none => True | some tr => t < tr)
20