permits
permits defines a boolean predicate on a consent ledger that returns true precisely when at least one window in the ledger's list authorizes the given action at the specified time. Modelers of recognition-based consent in physical systems cite it when composing access rules over ledger structures. The definition is a direct one-line unfolding that applies List.any to the windows field using the permitsAt check from each ConsentWindow.
claimLet $L$ be a consent ledger over a type $A$ of actions, let $t$ be a natural number, and let $a$ be an action. Then permits$(L,t,a)$ equals true if and only if there exists a consent window $w$ in the list of windows of $L$ such that permitsAt$(w,t,a)$ holds.
background
A ConsentLedger is a structure whose sole field is a list of ConsentWindow entries. Each ConsentWindow carries a scope predicate over actions, a start time, an optional end time, and an optional revocation time. The permits definition operates directly on this list structure without additional hypotheses. Upstream results include the ConsentWindow structure that supplies the permitsAt predicate, together with the constant A from IntegrationGap and Masses.Anchor that fixes the active edge count per fundamental tick at 1.
proof idea
This is a one-line definition that applies List.any to the windows field of the ConsentLedger, testing ConsentWindow.permitsAt on each window for the supplied time and action.
why it matters in Recognition Science
The definition is invoked by the lemma permits_append in the same module, which distributes the check over concatenation of window lists. It is also used in Unification.RecognitionBandwidth for the theorems demandedRate_pos and eightTickCadence_eq, thereby linking consent windows to recognition bandwidth and the eight-tick cadence. In the Recognition framework it supplies the basic access predicate that feeds into gravity models such as temperature halving for ultramassive black holes.
scope and limits
- Does not define the internal logic or revocation semantics of individual consent windows.
- Does not prove monotonicity or other algebraic properties of the predicate.
- Does not connect directly to J-cost, defect distance, or the phi-ladder.
- Does not handle continuous time or non-natural-number timestamps.
formal statement (Lean)
60def permits {A} (L : ConsentLedger A) (t : Nat) (a : A) : Bool :=
proof body
Definition body.
61 L.windows.any (fun w => ConsentWindow.permitsAt w t a)
62