Lex
Author note. The author has a commercial interest in systems of the kind this paper describes.
Abstract
An institutional decision can depend on an exception, a later change in law, or a judgment that only a competent authority may supply. A filing, for example, may satisfy an authorized extension while missing its original deadline. Computing the dates leaves the authority and scope of that extension to be established. Lex is a language that records what kind of answer or evidence each expression supplies. It distinguishes recorded events from derived legal consequences, attaches conclusions to the authority asserting them, and records precedence between rules and exceptions. When a decision needs authorized judgment, evaluation suspends with an exact question and resumes with an authenticated answer. We give a core calculus and an executable fragment with separate typing and execution rules. In finite formal models, re-evaluation preserves recorded sources and composition retains outstanding obligations. These results identify the conditions under which parts of an institutional decision can be computed. Full language soundness and semantic adequacy remain open. Legal interpretation and authoritative inputs remain explicit premises.
1. A Decision and Its Reasons
Consider a company filing its accounts after the ordinary deadline. The filing date is a recorded event. Whether the filing is timely may also depend on a written extension, issued for this company and this accounting period. An application for an extension and a granted extension have different legal consequences. A granted extension may change the filing deadline while leaving separate content, approval, and audit duties in force. Section 7.7 develops this example under the Companies Act 2006.
The calculation must therefore retain more than a date comparison. It must establish which rule applies, which notice has legal effect, and which obligations that notice changes. If a judgment is still required, the calculation must identify the question and who may answer it. Once answered, that question must remain linked to the company, period, rule, and evidence on which the answer depends.
Four distinctions arise from this example. First, an exception can defeat a general rule without replacing the rule itself. We call this defeasibility. A specific exception and a later enactment may both affect a decision, but their authority has different grounds. The first concerns the precedence of applicable rules. The second concerns which law governs at the relevant time.
Second, a historical event and its legal consequence have different stability requirements. The original filing date remains part of the record when an extension changes the assessed deadline. Lex gives these two kinds of time different types. A later calculation can then retain the event from which its conclusion was derived.
Third, a conclusion belongs to an asserting authority. A regulator and a treaty body may reach different conclusions about the same facts. For another institution to use either conclusion, it needs the issued act and the rule permitting that use. Recognition must preserve which authority supplied the evidence and which authority made the receiving decision.
Fourth, some questions require judgment. A determination such as “fit and proper,” “material adverse change,” or “good cause” cannot be supplied by an arbitrary Boolean value without losing its authority. We represent an unanswered question by a typed discretion hole. Its type specifies the answer required. Its authority and scope specify who may supply that answer and what the answer can resolve. Evaluation continues after a signed answer passes those checks.
Ordinary programming languages can implement each distinction. The language-design question is whether the distinctions remain explicit when independently written rules are combined. A reader of the final decision should be able to recover the applicable rule, the exception, the source evidence, and each authorized judgment from the derivation. Lex places this structure in the language and its typing rules.
Catala’s default calculus provides the closest comparison: it makes statutory exceptions explicit and links executable rules to legal text (Merigoux, Chataing, and Protzenko, 2021). The present question adds independently asserting authorities, changing legal consequences, and scoped human judgment. Section 10 compares these choices with Catala, authorization logic, and other approaches to computational law.
The calculus computes consequences relative to stated rules and accepted evidence. It does not supply the interpretation of a statute or create the authority of an officer. The next section identifies where computation ends and judgment begins. The later formal sections state the guarantees of the construction and their remaining limits.
2. What Kind of Law is Computable?
H.L.A. Hart’s The Concept of Law (1961) established that every legal rule exhibits open texture: a core of settled meaning surrounded by a penumbra of genuine uncertainty. “No vehicles in the park” prohibits a truck; whether it prohibits a motorized wheelchair or a decommissioned tank on a plinth as a memorial is indeterminate as a matter of the rule itself. The penumbra survives careful drafting because it is a structural feature of general language applied to a world of infinite particularity.
Dworkin’s Taking Rights Seriously (1977) and Law’s Empire (1986) argued that law is not exhausted by rules. Legal systems contain principles (“no one should profit from their own wrong”) that do not have enumerable exceptions; they have weight. How much pull a principle exerts in a given case is a matter of judicial interpretation. Constitutional law, common law reasoning, and interpretive jurisprudence resist formalization because the phenomena are constituted through interpretation.
The paper takes these interpretive questions as external premises. A program can use an interpretation supplied through an authorized procedure. The computation does not establish that interpretation’s legal authority. This distinction also applies when a court changes its reading of an unchanged constitutional text.
Other legal questions admit a finite calculation once the relevant facts, interpretation, and applicable exceptions are fixed. Consider Section 130(1) of the Seychelles International Business Companies Act 2016: “A company shall at all times have at least one director appointed in accordance with this Act, except where otherwise provided by another written law of Seychelles.” This is a predicate over a registered company producing one of two values {Compliant, NonCompliant}. Evaluation requires the directors collection and, for each director, the basis of the appointment; s.133(1) of the Act provides that a director shall be an individual or a body corporate, so no natural-person test enters. With appointment status and the applicable exceptions supplied, the remaining roster test is mechanical. The computation retains those supplied facts and interpretations as premises.
The drafting supplies more than the predicate. “At all times” is a temporal envelope rather than a point test (Section 3.2). Subsection (2), which disapplies the requirement for the period between incorporation and the appointment of the first directors, is an exception the legislature wrote, so its precedence over the base rule is enacted rather than assigned by whoever encodes the rule (Section 3.1). The closing “except where otherwise provided by another written law of Seychelles” is a reference out of this rule pack—a versioned collection of rules—and into another (Section 3.3). Three of the five properties of Section 3 are already on the face of one section of enacted text.
As a schematic example, take “file your annual return within 28 days of your fiscal year end.” Add an exception for bankruptcy and a further exception for a contrary court order. Once the relevant status and order are supplied, evaluation selects the applicable deadline. The example illustrates nested exceptions, without asserting a further statutory filing requirement.
Administrative and regulatory compliance rules can be computed where their relevant facts and authorized judgments are explicit. Statutes enumerate their own relevant fact spaces. The Pakistan Companies Act does not require knowing the weather in Karachi; it requires knowing whether the company has a registered office service provider and whether its directors meet the statutory qualifications. The type signature makes the reduction explicit.
Typed holes distinguish three states. Within the core of settled meaning the evaluator encounters a MechanicalHole and discharges it by ordinary typing and reduction. Where the rule reaches an open-textured determination (“fit and proper person,” “adequate systems and controls”) and a competent authority exists to answer, evaluation halts at a DiscretionHole: a person of specified authority supplies a judgment of specified type. Where the law has no disposition and no officer may lawfully invent one, Lex marks an UnsettledHole that clears only by a rule-pack rewrite issued through legislative or regulatory action. Hart’s penumbra and Dworkin’s harder cases remain explicit.
3. Five Properties of Compliance Rules
The filing example separates rule precedence, historical events, changing law, institutional authority, and judgment. Each distinction needs a representation that later computations can inspect. We first develop those representations through rules and evidence. Section 4 then gives their typing and execution rules.
A type states what kind of value or evidence an expression supplies. Writing e:A means that expression e has type A. A witness is the evidence required by a stated rule. Checking a witness establishes that rule’s premises within the model. The authority and legal interpretation of the rule remain external inputs.
3.1 Defeasibility
The example uses Abu Dhabi Global Market (ADGM) and its Financial Services Regulatory Authority (FSRA). Authorization status supplies the base result, and an admitted exemption supplies the exception condition.
A defeasible rule has a base conclusion that holds unless a higher-priority exception applies. In Lex, exceptions are not control flow. They are independently meaningful rules with explicit numeric priority:
lambda (ctx : IncorporationContext).
defeasible
(match ctx.fsra_authorization_required return ComplianceVerdict with
| False => Compliant
| True => match ctx.fsra_authorization_status return ComplianceVerdict with
| FullLicense => Compliant
| InPrincipleApproval => Pending
| _ => NonCompliant)
priority 0
unless
(guard: ctx.regulated_activity_exemption,
body: Exempt, priority: 1)
endThis encodes a rule of the type found in the ADGM Financial Services and Markets Regulations 2015 (FSMR, s.28). The base rule (priority 0) requires FSRA authorization. The exception (priority 1) exempts entities with a regulatory exemption. Priority is explicit, not positional.
Evaluation visits the base, each guard, and each satisfied exception body in source order. The highest-priority satisfied exception determines the outcome. If no exception fires, the base body supplies the verdict. This directly encodes lex specialis: the exception at priority 1 defeats the general rule at priority 0. Lex posterior is handled by temporal stratification (Section 3.2), not by defeasibility: the two principles operate on independent axes.
In the core calculus (Section 4), a defeasible rule is a term with a base type, base body, and a list of exceptions, each carrying a guard, a body, and a priority. The typing rule requires all exception bodies to inhabit the same type as the base body, ensuring that defeasibility does not change the type of the result.
3.2 Temporal Stratification
An extension changes the deadline calculated from a filing period. The recorded period and filing date remain available for later review. To express this distinction, Lex uses two types of time value:
Time_0 (frozen historical time): a retained assertion of a time, such as “The company was incorporated on 2024-03-15.” Event occurrence, judgment signing, and bulletin anchoring have distinct roles and records, although each uses this sort. Later evidence may dispute an assertion; the original record remains available.
Time_1 (derived legal time): time produced from a frozen fact by a legal rule. A filing period ended on 2022-06-01 (
Time_0). The filing deadline derived from that fact isTime_1; tolling rewrites that deadline into a furtherTime_1. The event time is unchanged by either derivation.
A rule pack records the rules used for one evaluation, their repeals, and their effective date. A rewrite witness records the justified passage from one such pack to another. The next subsection defines both objects. Here they identify which law produced a deadline. A bulletin is an authenticated public log. A proof-carrying authorization, abbreviated PCAuth in the rules, records an authorized answer and its signing time. Section 3.5 defines that record.
A constructor is a specified way to build a value. The temporal constructors record which inputs justify each time value. Their graph has an edge from an input type to the output type of a constructor. The following result checks the direction of those edges. It does not yet cover every expression of the full language.
The critical invariant is directional: lift_0 coerces Time_0 into Time_1 (frozen facts can produce derived consequences), but no constructor coerces Time_1 back to Time_0. The mechanized result is a rule-graph theorem about the temporal constructors named in this paper, not a completed embedding theorem for the entire has_type relation. Lex carries a typing judgment, where G lists the available assumptions and the expression after the colon states the assigned type: G |- t : Time_i whose intended i = 0 derivability is closed under exactly the Time_0 introduction forms (date literals, EffectiveDate, the Time_0 component of bulletin stamps and PCAuth timestamps). The closed theorem is that the temporal rule graph contains no Time_0-introduction edge with a Time_1 premise and no generated coercion path from Time_1 to Time_0:
Theorem (temporal rule-graph non-regression). In the object-language temporal constructor graph generated by Lift, Derive, Toll, EffectiveDate, bulletin timestamps, PCAuth timestamps, and pack re-evaluation, no primitive rule with conclusion Time_0 has a premise of grade Time_1, and the reflexive-transitive closure of primitive temporal coercions contains no path \mathrm{Time}_1\to\mathrm{Time}_0. The temporal sorts are abstract and are not scrutinees of Match-Dep.
Proof. By finite inspection of the temporal rule grammar. The introduction forms for Time_0 are: date literals (no temporal premises), EffectiveDate(r, t_0) whose only temporal premise is t_0 : Time_0, and the Time_0 component of BulletinStamp and PCAuth.timestamp records (also of Time_0 premise type). The metalevel projection src_0(derive_1(t_0, w)) returns the original source fact, but it is not an object-language eliminator from arbitrary Time_1 terms; it is a projection from the derived-time closure used in the metatheory. No Time_0-introduction rule has a Time_1 premise. The Rocq mechanization is TemporalStratification.v: no_time1_premise_to_time0_rule proves that no temporal rule with Time_0 conclusion has a Time_1 premise; temporal_non_regression lifts this over temporal derivation trees; and no_temporal_retract proves that the generated temporal coercion graph has no path from Time_1 back to Time_0. The remaining full-typing coverage theorem, from the complete has_type relation into this temporal rule graph, is a metatheoretic integration obligation.
No primitive rule eliminates Time_1 into Time_0. A constant function of type Pi(x : Time_1). Time_0 is derivable, but its result is built from Time_0 introduction forms alone. Proving that such a result cannot depend on x is a separate non-interference theorem and remains open.
This models a real legal invariant. Retroactive legislation changes the consequences of past events, not the occurrence of past events. The Companies Act can be amended to change the filing deadline for companies incorporated in 2024. It cannot be amended to make those companies not have been incorporated. Time_0 records what happened. Time_1 records what the law says about what happened. The two are related by explicit forward coercion and by metalevel derived-time closures, but never by an object-language demotion.
Effective dates, repeal, tolling, and rule-pack evolution are therefore terms, not metadata. The temporal layer gives them explicit types: EffectiveDate(r, t_0) : Time_0, Pack(id, version, rules, repeals, effective_date) : PackType, Rewrite(P -> P’) : RewriteWitness, Repeal(rule_ref) : RepealWitness, derive_1(t_0, P, w_P) : Time_1 for a derivation witness w_P : DerivationWitness(P) (Section 3.3), and Toll(d, delta) : Time_1 for an admitted exclusion delta : QualifiedExclusion(d). Its elapsed duration is computed from the qualified support, as detailed below. A rule may be evaluated for an event at time t_e only when its effective date is no later than t_e. A repeal tombstone blocks a fresh active-rule proof at and after its own effective date.
Retroactive invalidation and repeal. The stratification bears directly on retroactive invalidation, where an authority strikes down or reinterprets a rule with effect backward in time. The paradigm example is Schrems II (Court of Justice of the European Union, C-311/18, 2020), in which the EU-U.S. Privacy Shield framework was invalidated with immediate effect for all transfers then in progress. An entity that had relied on Privacy Shield certification as its basis for a data-privacy verdict on 2020-07-01 could, the following week, be evaluated against a legal framework in which Privacy Shield never provided a valid basis. A naive compliance system conflates these two evaluations.
Lex types that transition directly. Let P_shield be the pre-invalidation pack and P_schrems the post-invalidation pack. The invalidation is a typed witness Rewrite(P_shield -> P_schrems) induced by Repeal(privacy_shield_basis) with its own effective date. A verdict already derived under P_shield remains a well-typed Time_1 object: it is a record of what the law said under that pack. A fresh evaluation of an event after the repeal date, or an explicit reevaluate(-, Rewrite(P_shield -> P_schrems)), uses the rewritten pack. The weak claim remains syntactic: no constructor coerces a Time_1 value back to Time_0. The stronger claim, that derived consequences can be recomputed under a new pack, is internal to the typed temporal layer.
Stacked tolling. Let d : Time_1 and delta_1 : QualifiedExclusion(d). Then d_1 := Toll(d, delta_1) is a derived deadline. A second delta_2 : QualifiedExclusion(d_1) gives Toll(d_1, delta_2) : Time_1. Each exclusion carries its qualifying interval and evidence. Section 7.8 computes the elapsed effect from their normalized union, so repeated or overlapping support contributes time once. Nesting retains the base deadline and distinct legal grounds. No toll rewrites the historical event time.
A change can also take effect at different times for different institutions. We write [A]v for a conclusion v carried with authority A’s evidence. Section 3.4 develops this notation. A bridge witness supplies the rule and evidence that permit a receiving institution to use a source conclusion.
Authority-relative temporal divergence. Temporal change is authority-indexed. If authority A moves from pack P_A^0 to P_A^1 at t = 100 while authority B does not move from P_B^0 to P_B^1 until t = 120, then an event e at t = 110 may simultaneously inhabit [A] v_A and [B] v_B with v_A != v_B. This is not inconsistency: the verdicts live under different tribunal modals. Reconciliation, where it exists, requires an explicit bridge witness carrying one verdict across the authority boundary. Where no bridge witness exists, the divergence is a first-class obstruction.
Temporal obligations. Lex includes pointwise temporal proposition formers for admissibility-time claims: diamond phi (eventually phi) and box phi (always phi) over the finite rule-evaluation horizon. Temporal logic over execution traces is not proved here. In particular, behavioral obligations in linear temporal logic (LTL), computation tree logic (CTL), or timed computation tree logic (TCTL), including a full until connective over Op traces, are open at the Lex-to-Op boundary. Lex keeps quantitative time bounds in typed time objects and effective-date guards; it does not claim a complete trace semantics.
Two claims must be separated. The weak claim, discharged within the calculus, is that historical facts cannot be overwritten by later legal rewrites. This is syntactic: no constructor exists that coerces a Time_1 value back to Time_0, so a retroactive legal change can alter derived legal consequences while preserving the record of what happened. The stronger claim, that derived consequences can be recomputed under pack evolution, can be stated inside the metatheory once rule packs and rewrite witnesses are made typed objects. The next subsection gives that formalization. What remains open is the full proof that the pack-evolution construction commutes with the modal and temporal subsystem without introducing a hidden \mathrm{Time}_1\to\mathrm{Time}_0 path.
3.3 Pack Evolution
Temporal stratification prevents later law from rewriting frozen history. A second invariant is needed when the law itself changes: the rule pack against which a derivation was produced must be explicit enough that the derivation can be replayed under a later pack without inventing new historical facts.
A derivation records successive applications of rules to their premises. The notation below makes the selected pack part of that record. Here G lists the available assumptions, e is the expression being checked, and A is its required type. When typing or evaluation depends on a particular pack, write G |-P e : A for the ordinary Lex judgment relative to the rule constants supplied by P.rules. The pack itself is the typed object
Pack(id, version, rules : Set Rule,
repeals : Set (RuleRef x Time_0), effective_date : Time_0) : Type_0with id : PackId, version : N, rules : Set Rule, repeals : Set (RuleRef x Time_0), and effective_date : Time_0. Pack is therefore a versioned snapshot of the statutory or regulatory corpus together with the historical date from which that snapshot is legally live. Its repeal set carries tombstones rather than erasing history.
A name such as “the filing rules” can denote different text at different times. Re-evaluation needs an identifier for the exact rule content used in the earlier decision. The digest below supplies that identifier under the stated hash assumption.
Pack digest and content-addressing. PackId is the content-addressed digest of the pack’s defining content: id = digest(canonical_encoding(rules, repeals, effective_date)) under a fixed collision-resistant hash. Two packs with the same id are the same pack as far as Lex is concerned. The version : N field is an authority-assigned monotone label; it is not the pack’s identity. Rule identity is also digest-based. Thus r in P.rules is decidable when the canonical rule encoding is decidable. The Lex and Op layers commit to the same pack digest.
Cross-pack reference. A statute that defers to another written law, as s.130(1) of the Seychelles Act does in its closing words (Section 2), refers out of its own pack. Lex types the reference through the pack index of the judgment. A rule constant is a digest, so a rule of P may cite a rule q of a coexisting pack Q by digest, and a derivation that uses both is the judgment G |-{P,Q} e : A, the ordinary judgment relative to the rule constants supplied by P.rules ∪ Q.rules; Rule-Active (Section 4.5) must then hold for q in Q at the event time, so the deferred-to law is live on its own effective date and not on the citing pack’s. The reference is to an exact rule body, never to a name that a later edition may rebind: when Q evolves by Rewrite(Q -> Q’), the cited digest either survives in Q.rules ∩ Q’.rules or is repealed, and the replay-transport obligation below governs the derivation exactly as it governs a rule of P. Which law prevails when both speak is a separate question, settled by the precedence structure of Section 3.1 when the deferring clause is an exception written into the citing rule, as it is in s.130(1), and by the cross-statute meet of Section 7.4 when two laws reach the same domain with independent requirements.
A pack rewrite is a typed transformation
omega : Rewrite(P -> P') : RewriteWitnessIts sole constructor takes four proofs.
Conservativity. Every rule in
P.rulesis either still present inP’.rulesor has a tombstone(r,t_rep)inP’.repeals. New rules may be added freely.Type preservation. If a rule
ris active in both packs, thentype_P(r) = type_P’(r).Effective-date monotonicity.
P’.effective_date >= P.effective_date.Replay transport. For every derived-time witness that the rewrite claims to preserve, the rewrite carries a function transporting a
DerivationWitness(P)into aDerivationWitness(P’). If a cited rule is repealed and no replacement proof exists, no replay witness exists for that derivation; re-evaluation is then blocked rather than silently coerced.
The witness is typed because a syntactic patch to the rule text is not enough; one must also prove that the pack boundary moved forward in time and that surviving rules did not silently change type. RewriteWitness is inhabited only by such pack rewrites, and only the re-evaluation operator below consumes one. The witness a single derivation cites is a different object, typed next.
Write w_P : DerivationWitness(P) for a derivation witness: a record whose cited rules all lie in P.rules, by digest, and whose legal effect is valid no earlier than P.effective_date. Where a derivation cites several packs, as in the cross-pack judgment above, the index is the finite set of packs cited, P.rules reads as the union and P.effective_date as the latest of the packs’ effective dates, and Rewrite(Q -> Q’) transports a DerivationWitness({P,Q}) to a DerivationWitness({P,Q’}) by transporting its Q component alone. The derived legal time derive_1(t_0, P, w_P) therefore records the frozen fact t_0 : Time_0, the pack under which the consequence was derived, and the pack-relative witness that justifies the consequence. This three-place closure is the canonical form. Write DerivedTime(P) for the type of such closures under P; Lex has no subtyping (Section 4.11), so DerivedTime(P) is not a second type for the closure: G |- d : DerivedTime(P) abbreviates G |- d : Time_1 together with d ≡ derive_1(t_0, P, w_P) for some t_0 and w_P, up to beta and zeta reduction, and it is the domain of reevaluate below; a let-bound derived deadline, as in Section 7.7, meets the premise by zeta. Because the witness type carries its pack index, derive_1(t_0, w_P) abbreviates derive_1(t_0, P, w_P) with P read off the witness, and every two-place occurrence in this paper is that abbreviation; in the worked examples of Section 7 the witness is written as a named record whose pack field carries the index.
The re-evaluation operator is the metalevel map
reevaluate : DerivedTime(P) x Rewrite(P -> P') -> DerivedTime(P')defined by
reevaluate(derive_1(t_0, P, w_P), omega) :=
derive_1(t_0, P', replay_witness(omega, w_P))where w_P’ is obtained by replaying the same Time_0 witness through the active rules of P’ justified by omega. This is not a term-former \mathrm{Time}_1\to\mathrm{Time}_0 inside the object language. It is a metalevel operation on a derived-time closure that already stores the originating t_0. For general Time_1 values, Lex uses a structured source-history map: lift_0(t_0) contributes a lift event, a derived closure contributes a derive event carrying the source time, pack id, witness digest, and rule digests, and Toll(d,delta) appends the admitted exclusion and its normalized support. The closed re-evaluation theorem preserves the source-time projection and records the new derivation pack; the full stable-fragment translation of arbitrary terms remains the open pack-evolution obligation below.
Define the metalevel projection src_0(derive_1(t_0, P, w)) := t_0.
Replaying an unchanged pack should leave the result unchanged. Replaying two successive rewrites should agree with replaying their composition. These are the identity and composition laws meant by functorial below. The source-time projection records the historical input that both replay paths must retain.
Proposition (re-evaluation is functorial). Re-evaluation preserves source time and effective-date monotonicity. It also satisfies reevaluate(d, id_P) = d and reevaluate(reevaluate(d, omega), omega’) = reevaluate(d, omega’ ∘ omega) whenever the rewrite witnesses compose.
Proof. A derived legal time is the closure (t_0, P, w_P). Re-evaluation changes the pack and replays the witness while leaving t_0 fixed. Identity and composition follow from identity and composition of witness replay. Effective-date monotonicity is a field of each rewrite witness and is transitive under composition. PackReevaluation.v closes these facts as src_0_reevaluate, reevaluate_id, reevaluate_compose, and rewrite_effective_date_preserved; re_evaluation_soundness is the defining equation.
The preceding proposition concerns closures that already store their source time and replay witness. A general program also has variables, functions, and branches. Transporting all of those expressions requires a further theorem. The next obligation isolates programs whose cited rules survive unchanged.
On the omega-stable fragment, where every rule constant appearing in G, e, and A lies in P.rules ∩ P’.rules. The intersection is taken over rule digests, not over rule identifiers. Define the translation tau_omega by tau_omega(r) = r on preserved rule constants and extend it homomorphically to contexts, terms, and types. Write G’ = tau_omega(G), e’ = tau_omega(e), and A’ = tau_omega(A). The digest discipline is what makes “the same rule survives” a checkable side-condition: a rule whose digest is unchanged has verbatim-identical body, types, and priority metadata in both packs, so the homomorphic translation is literally the identity on preserved rules.
Open obligation (pack-evolution soundness, stable fragment). If G |-P e : A and omega : Rewrite(P -> P’), every rule constant used in the derivation of G |-P e : A has its digest in P.rules ∩ P’.rules, added rules in P’ are inert for the translated derivation, and omega carries replay witnesses for every pack-relative derived-time closure used by the derivation, then G’ |-P’ e’ : A’. If evaluating e under P and evaluating e’ under P’ both terminate in compliance verdicts, the two verdicts are equal.
Required proof. Induct on the typing derivation. The pack-sensitive leaves are rule constants and witnesses carried by derive_1. By hypothesis every such rule survives in P’; by the type-preservation obligation in omega, it has the same type in both packs, and by replay transport the derived-time witness can be rebuilt under P’. Every other constructor is translated homomorphically, so the ordinary induction for variables, lambda, application, let, match, and defeasible rules should go through unchanged. Verdict preservation also requires an operational inertness argument: added rules in P’ do not fire for this derivation.
Worked example: Pakistan Companies Ordinance, 1984, and the 2010 fee rewrite. Let P_84 be the Sixth Schedule fee pack for the Companies Ordinance, 1984, and let P_10 be the pack made effective on 2010-10-26 by S.R.O. 996(I)/2010. The baseline Sixth Schedule charged Rs. 200 for filing a document or return other than a charge instrument and Rs. 5,000 for recording a charge. The 2010 rewrite substituted Rs. 600 for an electronic non-charge filing, Rs. 1,500 for a physical non-charge filing, Rs. 5,000 for an electronic charge filing, and Rs. 7,500 for a physical charge filing.
Define a derived judgment under P as delta : P |- e ⇓ (t_1,v), where t_1 : DerivedTime(P) and v : ComplianceVerdict. Re-evaluating a judgment replays its witness and runs Eval-Rule under the new pack against the same frozen facts.
The first case produces the same verdict after re-evaluation. Let t_0^charge be the frozen filing fact “a company filed a charge-registration document electronically on 2010-11-15 and paid Rs. 5,000.” Under P_84, delta_84 : P_84 |- e_charge ⇓ (derive_1(t_0^charge,P_84,w_P84),Compliant). Re-evaluating with omega_84->10 : Rewrite(P_84 -> P_10) yields delta_10 : P_10 |- e_charge ⇓ (derive_1(t_0^charge,P_10,w_P10),Compliant), because the electronic charge fee is Rs. 5,000 in both packs.
The second case produces a different verdict. Let t_0^return be the frozen filing fact “a company filed an annual return electronically on 2010-11-15 and paid Rs. 200.” The stale judgment is delta_84 : P_84 |- e_return ⇓ (derive_1(t_0^return,P_84,w_P84),Compliant). Re-evaluation yields delta_10 : P_10 |- e_return ⇓ (derive_1(t_0^return,P_10,w_P10),NonCompliant), because the 2010 pack raised the electronic non-charge filing fee from Rs. 200 to Rs. 600. The filing fact is unchanged. The legal consequence changes.
Conjecture (pack-evolution soundness for the modal and temporal subsystem). The theorem above extends from the stable fragment to the full modal-temporal language: if G |-P e : A may contain the temporal modalities @t A, diamond t A, box[t1,t2] A, tribunal modals, and pack-indexed derived times, then every well-typed omega : Rewrite(P -> P’) induces translated judgments G’ |-P’ e’ : A’ that commute with reevaluate and preserve verdicts.
This is not proved here. The missing step is a single stratification argument showing that modal introduction and elimination commute with pack-indexed re-evaluation without creating either a hidden \mathrm{Time}_1\to\mathrm{Time}_0 path or a cycle in the admissibility predicate. The same obstruction is what requires the finite compiler model in §5.1 below to exclude the temporal coercions Lift0 and Derive1 from the Op compilation target: a derived time derive_1(t_0, w_P) carries the pack-relative witness w_P as part of its denotation, and Op has no operational-semantics-level primitive for transporting a pack-relative witness through a compiled trace until this conjecture is closed. The Lex admissible fragment (§5) and the finite compiler model therefore exclude temporal coercions for the same reason: neither layer can yet discharge the cross-pack commutation obligation this conjecture names.
3.5 Typed Discretion Holes
An unanswered question does not by itself identify what should happen next. A calculation may settle it, an authorized officer may decide it, or a change in law may be required. Lex distinguishes those cases at each hole site. Hart’s core of settled meaning is mechanical. Hart’s penumbra is discretionary: the law delegates judgment to an existing authority, and the answer has not yet been rendered. Dworkin’s harder cases are unsettled: the present rule pack has no disposition, and no officer may answer without changing the law itself. The three states:
Mechanical. The question lies within the core of settled meaning. The evaluator computes the answer directly, and the audit trail records that no human judgment was needed.
Discretion. The question lies in Hart’s penumbra. A legally recognized authority exists, but the answer has not yet been rendered. The derivation suspends pending a proof-carrying authorization witness.
Unsettled. The law has no present disposition. No authorized individual may supply an answer under the current rule pack. The derivation suspends pending legislative or regulatory change.
In the core calculus:
MechanicalHole(has_natural_person_director) : Bool
DiscretionHole(ADGM.FSRA, fit_and_proper) : ComplianceVerdict
scope { jurisdiction: ADGM, entity_class: AuthorizedFirm }
UnsettledHole(DigitalAssets, digital_beneficial_ownership) : ComplianceVerdictThe first shape is degenerate but important: a MechanicalHole marks a site that was once legally interesting but is now within the rule pack’s settled core, so the type checker discharges it automatically. A DiscretionHole(auth, h) marks a site where existing law delegates judgment to auth. An UnsettledHole(domain) marks a stronger failure: no lawful answer exists until the rule pack itself changes. It cannot be filled by an officer, board member, or regulator acting under the existing pack.
The answer must remain attached to the question that requested it. For the filing example, an answer about one accounting period must not resolve another period’s extension. The request therefore identifies the hole, expected answer, rule pack, and surrounding evidence. fill resumes evaluation using an answer and its authorization.
Only the discretionary case uses the existing fill path:
fill(fit_and_proper, Compliant, w) where w : PCAuth(auth, h, Compliant, request(h,Compliant))The authorization record below groups three checks. It identifies the signers and their delegated authority, binds the exact request and answer, and records the signatures and their public timestamps. A quorum is the required number of distinct authorized signers. The notation Vec n X means a vector of n entries of type X. A digest identifies exact encoded content. The later verification rule checks these fields together.
PCAuth (Proof-Carrying Authorization) is the quorum-indexed witness family binding the fill to its whole admission context: (1) the identity of each signer who supplied the judgment, (2) the authority under which each signer acts, (3) the scope in which the authority applies, (4) the exact hole and value, and (5) the request, pack, and proof-context digests against which the fill was solicited. This is the one record layout used throughout the paper. If hole h has type tau_h, v : tau_h, and r : FillRequest(auth,h,tau_h,pack_digest,context_digest), then PCAuth(auth, h, v, r) is the witness type:
FillMode(h) = Creative | Applied(PrecedentRef(h))
PCAuth(auth, h, v, r) = {
quorum : Nat, -- required signer threshold
signers : Vec n Did, -- Did identifies a signing principal
depth : Vec n Nat, -- realized delegation depths
authority : Vec n AuthorityChain(auth, signers[i], depth[i]),
scope_ok : ScopeWitness(chain_scope(authority) cap h.scope, v),
justification : Vec n (Option Text), -- optional public-facing reasoning
mode : FillMode(h), -- novel reasoning or precedent-guided
ledger_ref : LedgerRef, -- append-only justification ledger entry
timestamp : Vec n Time_0, -- when each judgment was made
anchor : Vec n LinkedTimestamp(hash(signatures[i])),
request_hash : FillRequestHash, -- digest of r
pack_digest : PackDigest, -- governing rule-pack digest
context_digest : ContextDigest, -- surrounding proof/context digest
payloads : Vec n PCAuthPayload(protocol_tag, canon_version,
hash_suite, sig_alg, signers[i], auth, h, v,
authority[i].chain_digest, digest(h.scope),
timestamp[i], request_hash, pack_digest,
context_digest, mode,
digest(justification[i]), ledger_ref),
signatures : Vec n Ed25519Sig(payloads[i]),
distinct : DistinctSigners(signers),
quorum_ok : quorum <= n
}We write PCAuth_k(auth, h, v, r) for the same witness type with quorum exactly k; the single-signer witness of the worked examples is the instance n = quorum = 1. The authority field records a bounded delegation chain from the root authority to each signer. The signature covers the one canonical payload shown in the record. The anchor is not signed; it commits to the completed signature in the public log. No free value parameter remains. DistinctSigners prevents duplicate signer counting; the signed request, pack, context, chain, and scope digests prevent replay across those boundaries.
Delegation can restrict which answers a signer may supply. A hole can impose further restrictions. An accepted answer must satisfy both. This is why scope uses intersection: combining restrictions retains every restriction from either source. The order compares permission sets by inclusion. The formal name for this structure is a meet-semilattice.
Scope is a meet-semilattice element, not a record shape. Fix once for the rest of the paper: a Scope for a hole h of value type tau_h is a decidable downward-closed predicate S : Pi x : tau_h. Prop; the semilattice operation S cap S’ is pointwise conjunction ((S cap S')(x) := S(x) /\ S'(x)), the top element is the constantly-true predicate, and inclusion S subseteq S’ means pointwise implication.
Pointwise implication between arbitrary decidable predicates is not itself decidable, so the delegation check that uses it needs a stated fragment and a procedure rather than an appeal to entailment in general. Two suffice for the caveat kinds this paper uses. Where a caveat is monotone in its parameters — a cap, a deadline, a jurisdiction list — inclusion is structural subsumption: compare the parameters directly, and a tighter cap or an earlier deadline entails a looser one with no search at all. Where it is not, enumerate the finitely many contexts generated by the literals appearing in the parent and child predicates and check the implication on each; this is sound and complete for that fragment, because a predicate over those literals cannot distinguish contexts agreeing on all of them. Both are deliberately not a call to an external solver: an answer from a satisfiability modulo theories (SMT) solver would have to be trusted or re-checked, and a delegation check resting on an unverified oracle is not a proof term.
A ScopeWitness(S, v) is a proof term of S(v). Concrete presentations such as { jurisdiction: ADGM, entity_class: AuthorizedFirm } (§7.5) are named atomic predicates joined by cap; they are surface sugar for elements of this lattice. Fill-time checking is the value check ScopeWitness(chain_scope(w) cap h.scope,v): the signed value lies in both scopes. Predicate inclusion is checked once when a delegation edge is issued. Throughout, scope is neither a type nor a record.
The authority field is the critical trust anchor. Each chain is witnessed by the authority named in the hole; it is never self-asserted. The intended resolution is an identity primitive: a verifiable credential attesting that a specific person holds a specific role (e.g., “FSRA-authorized compliance officer”) at the authority named by auth. The optional justification entries are audit-relevant text explaining the reasoning. Justifications are published to an append-only ledger, addressed by ledger_ref, so later reviewers can inspect why a fill was made. The mode field distinguishes Creative fills, where the authority advances novel reasoning, from Applied fills, which cite an existing precedent reference.
There are two distinct security questions. The verifier may check all required fields correctly, yet an attacker may still exploit a broken signature scheme or wrongly issued credential. The finite counting result below separates these failure classes. EUF-CMA is the standard signature-forgery experiment: the attacker must sign a fresh message after obtaining signatures on messages of its choice. The later reduction states the remaining connection to that experiment.
Proposition (finite discretion-hole event-union bound). Under a finite observation space and a constructed reduction mapping every hole-forgery observation either to an EUF-CMA signature-forgery observation or to a credential-chain overhead observation, the number of successful hole-forgery observations is bounded by the sum of the two target counts. The counting lemma closes in PaperMechanization.v as finite_observation_event_union_bound. Instantiating the abstract event predicates with Ed25519 EUF-CMA games and a concrete credential-issuance verifier remains the cryptographic binding step.
Proof sketch. A forged witness either contains a forged signature on the canonical payload or a valid signature from a credential issued outside the authorized procedure. The anchor commits to the completed signature and is verified separately. The finite event-union lemma bounds the two failure classes; binding them to Ed25519 and credential issuance remains open.
Op: Compliance-Carrying Operations (Lorgat 2026c) fixes the target proof-bundle transport form of this witness. The current mechanized fill case treats the witness as an uninterpreted authority/digest/timestamp payload transported through compilation; delegated revocation, expiration, multi-signer quorum transport, bulk verification, and cross-jurisdiction bridge validation remain open unless separately cited as closed.
Revocation is a separate typed artifact, Revoke(c) : RevokedCred, signed by the issuer of c and bulletin-stamped at a public time. A verdict’s revocation status aggregates its complete authority dependencies. Any revocation at or before the relevant source anchor makes that dependency Invalid. A later revocation gives Tainted only when no dependency is invalid. Section 4.9 defines the unique aggregate tag and its evidence requirements. Comparable authenticated bulletin positions supply the order. Missing coverage or comparison evidence leaves classification pending.
The intended security reduction has two institutional assumptions: the cryptographic soundness of the signature scheme and the administrative soundness of credential issuance. Both are standard targets for attack in a public-key credential system. Open problems below this level, revocation of PCAuth witnesses when a filer’s credential is later rescinded, root-of-trust establishment for a multi-authority corridor, are enumerated in Section 12. The obligation authenticates the author and integrity of the fill metadata; it does not certify the legal correctness of the justification itself.
PCAuth(auth, h, v, r) is a dependent record: its type fixes the authority, the hole, the exact value, and the fill request, with tau_h given by the hole signature of §4.7 and r committing the current pack and proof-context digests. fill supplies an inhabitant; VerifyPCAuth is the decision procedure that re-checks its defining data.
We write VerifyPCAuth(W, h, v, r, check) for the verifier judgment of signature PCAuth(auth, h, v, r) x HoleId x tau_h x FillRequest x AdmissionCheck -> Bool; it re-checks signatures on the canonical payload, binds the witness threshold to the hole policy required(h), checks signer membership in committee(h) and the deployment n_max bound, linked timestamp anchors, authority-chain validity, non-revocation of every credential in the authority chain at the admission/fill check snapshot, and the delegation depth bound. The AdmissionCheck input carries complete chain, revocation-coverage, and anchor-comparison evidence through its declared horizon. Preparing that input can return PendingEvidence. An inclusion path alone cannot establish non-revocation. The Boolean verifier operates only after evidence preparation succeeds. Later revocation preserves the historical fill and contributes to the unique aggregate status defined in Section 4.9.
Proposition (quorum acceptance unfolding). Let W : PCAuth_k(auth, h, v, r) and let VerifyPCAuth(W, h, v, r, check) accept against the hole policy. Then there exists a finite list Q of at least required(h) distinct committee attestations. Every a in Q has a valid Ed25519 signature on PCAuthPayload(protocol_tag,canon_version,hash_suite,sig_alg,a.signer,auth,h,v,a.chain_digest,digest(h.scope),a.timestamp,request_hash(r),pack_digest(r),context_digest(r),mode,digest(a.justification),ledger_ref). Its linked timestamp anchors the resulting signature. Its authority chain begins at auth, ends at a.signer, stays within the depth bound, and contains no credential revoked at the admission snapshot.
Proof. The verifier predicate is a finite conjunction of exactly these checks; take Q to be the accepted attestation list. Mechanized in PCAuthQuorum.v (quorum_acceptance_unfolding with six supporting lemmas). The result assumes a verifier record satisfying the stated predicates. Cryptographic unforgeability is the separate obligation below.
Open obligation (PCAuth forgery reduction). Fix a deployment in which the maximum quorum width is bounded above by n_max, as declared by the authority pack. Fix the verifier for PCAuth_k(auth, h, v, r) for any k <= n_max, and assume Ed25519 is EUF-CMA secure (Bernstein et al. 2012) with insecurity function epsilon_{Ed25519}(t) against time-t adversaries in the standard model. Let A be a probabilistic polynomial-time adversary running in time t_A that receives the public keys of n_max uncorrupted signers and outputs an accepted PCAuth witness containing a fresh signature. Let epsilon_A(t_A) denote its success probability. Let q_{\mathrm{sig}}\geq1 bound the total number of signing queries. The coarse overhead below also covers preparation of the bounded signer set. The target reduction constructs an Ed25519 adversary B running in time t_B = t_A + O(n_max · q_{sig}) such that
epsilon_{Ed25519}(t_B) >= epsilon_A(t_A) / n_max.Let c be the number of corrupted signers. The reduction concerns signer corruption, not legal correctness. If c >= k, a corrupted quorum can sign without violating EUF-CMA. A legally wrong payload signed by an authorized uncorrupted signer is also not a forgery. The threshold statement therefore assumes c < k, uncorrupted signers enforce their local authorization predicate, and the authority pack fixes the committee and revocation snapshots.
The loss is only the signer-slot guess. The extractor checks every attestation under the challenge key and therefore need not guess a position inside the accepted quorum.
Proof sketch. The reduction guesses one of the n_max uncorrupted signer slots and simulates every other key locally.
Slot guessing. The reduction
Breceives the EUF-CMA challenge public keypk_*, samplesi_* in {1, ..., n_max}uniformly, and embedspk_*in sloti_*. For every other slot,Bsamples a fresh Ed25519 keypair and retains the secret key.Hybrid simulation of signing queries. For any signing query
Aissues for sloti_*on a canonical PCAuth payloadmfor signers_{i_*},Bforwardsmto the EUF-CMA challenger and returns the response. For any signing query for a slotj != i_*,Banswers using the locally retainedsk_j. This perfectly simulatesA’s view of the signing oracle for all slots.Forgery extraction. When
Aoutputs an accepted witness,Binspects every attestation underpk_*. A signature on a canonical payload never submitted to the challenge oracle is an EUF-CMA forgery. Conditioned onAsucceeding, at least one uncorrupted slot contains such a signature. The slot guess therefore succeeds with probability at least1/n_max.Simulation. The adversary’s view is identically distributed because challenge-oracle answers replace local signatures only at the guessed slot. The reduction loses at most the
n_maxslot factor.
The runtime overhead O(n_max · q_{sig}) is the cost of locally answering signing queries for the n_max - 1 non-challenge slots and of constructing the n_max-slot public-key vector. This reduction is not mechanized in the current Rocq development; it is a cryptographic obligation whose adversary model, canonical-quorum extraction, credential-issuance assumptions, and bulletin assumptions must be fixed before it can be counted as a theorem.
If discharged, the bound is epsilon_A(t_A) <= n_max · epsilon_{Ed25519}(t_B). It is symbolic because n_max is fixed by each authority pack. The reduction is in the standard model.
Credential issuance, revocation, and delegation are therefore typed institutional objects rather than ambient side conditions. Their typing rules appear in Section 4.7, and Op re-checks them independently at dispatch.
Filled discretionary judgments can be lifted into first-class precedent values:
Precedent(fit_and_proper, past_fills) : PrecedentChain(fit_and_proper)This is consultative rather than binding. Following Levi’s An Introduction to Legal Reasoning (1949), precedent is reasoning by example: later fillers may consult the chain for guidance, cite it in an Applied fill, or depart from it with a Creative fill that begins a new branch. Lex types that distinction.
Filled discretionary judgments can also be appealed:
Appeal(fill_2025_01, ADGM.AppealsPanel)
: AppealedFill(fit_and_proper, fill_2025_01, ADGM.AppealsPanel)An appeal is a higher-authority re-fill of the same hole. The original fill remains in the record; downstream verdicts derived from it are tagged Appealed until they are re-derived under the higher-authority disposition. Revocation is typed supersession, not erasure.
The derivation trace can now distinguish three outcomes: fully mechanical evaluation, discretionary evaluation with an attributed judgment and public justification, and genuine unsettled law requiring pack evolution.
4. The Core Calculus
The examples require evidence whose type depends on a value: a jurisdiction, a filing period, or the exact question sent to an officer. Dependent type theory represents that dependence directly. It also provides rules for functions, pairs, propositions, and substitution. We use those rules to specify how the institutional constructions combine.
A typing judgment \Gamma\vdash e:A means that assumptions \Gamma justify assigning type A to expression e. The diagrams below place premises above the line and their conclusion below it. A judgment checks an expression’s form and evidence requirements. An execution rule separately states how evaluation proceeds.
Effects record the operations evaluation may perform. The institutional extensions then specify exceptions, time, authority, and judgment. Section 5 restricts this language to the executable fragment. Section 12 states the remaining mathematical obligations.
4.1 Universe Hierarchy
Types themselves need types so that the language can quantify over classes of evidence without making every expression interchangeable. A universe contains types at a specified level. Each universe includes the lower levels, and belongs to the next level. Lex uses three sort families, where a sort classifies a type or proposition:
Type_l for l = 0, 1, 2, …, the standard universe hierarchy for computational types.
Prop, the proof-irrelevant sort, living at Type_1. Propositions in Prop are erased at runtime; only their provability matters.
Rule_l, a documentation sort for compliance rules, stratified identically to
Type_l, with no additional typing discipline. The distinction is a semantic marker, normative rather than descriptive, that appears in diagnostic output and has no formal consequence in the typing rules.
Additionally, Time_0 and Time_1 are temporal sorts at universe level 0.
The typing rules for sorts:
------------------- (Sort-Type)
G |- Type_l : Type_{l+1}
------------------- (Sort-Prop)
G |- Prop : Type_1
------------------- (Sort-Rule)
G |- Rule_l : Type_{l+1}
------------------- (Sort-Time)
G |- Time_i : Type_0 (i in {0, 1})Sort-Rule is a documentation sort: compliance rules have the same hierarchical structure as types, and the marker is preserved through elaboration and diagnostic output but imposes no additional typing constraint. Sort-Time places both temporal sorts, frozen historical time and derived legal time, at ground level.
Universe levels are expressions built from natural number literals, level variables, successor (l + n), and maximum (max(l1, l2)). The metatheoretic universe hierarchy is countably infinite, indexed by \mathbb{N}. The implementation imposes a finite bound on absolute level values for efficient level resolution, and this bound does not affect the metatheory.
Prop Sort
A checked proof may justify accepting a value without being needed when that value executes. Erasure removes such proof data. It must preserve the data that execution uses, including decisions, signatures, and authority references. The rules in this subsection specify which logical constructions permit that separation.
Lex follows ordinary Coq-style Prop rather than a judgmentally proof-irrelevant sort: proof irrelevance is propositional, not definitional. Following Martin-Löf (1984), Werner (1997), and Pfenning (2001), proof terms in Prop participate in typing and in the identity type; runtime evaluation erases them. We write bottom_prop : Prop for propositional falsity, not P for P -> bottom_prop, and P or Q for proof-irrelevant disjunction.
The identity type Id(A,x,y) expresses equality of two A-values. Its constructor refl(x) proves that x equals itself. The eliminator J permits reasoning from an equality proof by reducing the reflexive case. Its motive C states which conclusion that reasoning must establish.
G |- A : S S in {Prop, Type_i} G |- x : A G |- y : A
-------------------------------------------------------------- (Id-Form)
G |- Id(A, x, y) : Prop
G |- x : A
--------------------------- (Id-Intro)
G |- refl(x) : Id(A, x, x)
G, x:A, y:A, p:Id(A, x, y) |- C(x, y, p) : S S in {Prop, Type_i}
G, z:A |- d(z) : C(z, z, refl(z))
G |- a : A G |- b : A G |- q : Id(A, a, b)
------------------------------------------------- (J)
G |- J_{C,d}(q) : C(a, b, q)Identity is intensional Martin-Löf identity with the ordinary eliminator J; no univalence axiom or higher-path structure is assumed. The erasure theorem below covers J only when its motive lies in Prop, or when its scrutinee is closed and reduces to refl. General equality transport into computational data remains outside the erasure fragment.
G |- P : Prop G |- p : P G |- q : P
----------------------------------------- (Prop-Irrelevance)
G |- proofirr(p, q) : Id(P, p, q)
Dec(P) ::= Yes(p : P) | No(n : P -> bottom_prop)
G |- P : Prop G |- d : Dec(P) [empty]
------------------------------------------- (Dec-LEM)
G |- decide(d) : P or not P [empty]Prop-Irrelevance is the proof-irrelevance commitment: for any two proofs of a proposition, Lex can construct a proof that they are equal. This is not a conversion rule. Two proofs may remain judgmentally distinct even when proofirr(p, q) inhabits Id(P, p, q); the equation is propositional rather than definitional. This matches ordinary Coq Prop rather than SProp.
Decidable propositions. A decision contains a checked positive or negative result. It lives in Type, so its branch survives erasure. Dec-LEM introduces the left disjunct from Yes(p) and the right disjunct from No(n). The rule consumes a decision. Producing that decision is a separate computation with its own immediate and latent effects.
Classical calculation. A Boolean formula is generated from atoms with admitted decisions. Its constructors are truth, falsity, negation, conjunction, disjunction, implication, and finite quantifiers. Each atom binds its predicate, value inputs, rule interpretation, and immutable evidence view. A total pure decision procedure returns a proof of its selected alternative. Finite encodings, signature checks, and complete finite decision tables supply useful instances.
The elaborator constructs decisions recursively. Negation exchanges the alternatives. Conjunction requires two positive results. Disjunction requires one. For implication, a negative antecedent or positive consequent proves the implication. A positive antecedent and negative consequent refute it. Finite quantifiers use the certified searches of Section 4.2. The surface classic form invokes this construction:
G |- b : BooleanFormula(atoms)
G |- decisions : Decisions(atoms) [empty] P = interpret(b)
------------------------------------------------ (Classic-Boolean)
G |- classic(b,decisions) : P or not P [empty]Classical calculation remains available for certified Boolean formulas. General Prop retains intuitionistic rules. An unresolved judgment supplies no negative decision. Classical reasoning in the mathematical metatheory adds no object-language rule.
The model used below records how available information grows. A proposition selects the contexts in which it holds, called a subobject of the context. Reindexing means evaluating the same proposition after substituting its inputs. The proof shows that an admitted decision gives complementary positive and negative cases, and that substitution preserves this split. Section 9 develops the model.
Proposition (sound classical calculation). Interpret Prop over a context \Gamma by subobjects of \Gamma in the presheaf model. Every admitted decision and every Classic-Boolean derivation is valid in this interpretation. Their interpretations commute with context substitution.
Proof. A section of \operatorname{Dec}(P) splits \Gamma into the positive subobject U and its negative alternative. These subobjects are disjoint and cover \Gamma. The negative alternative is therefore the Heyting complement \neg U, so U\vee\neg U=\Gamma. Pullback preserves the split. Complemented subobjects form a Boolean algebra. The decision constructors realize its operations. Induction over the formula proves the claim. An explicit finite enumeration reduces its quantifiers to finite conjunctions and disjunctions. \square
A missing observation supplies no negative decision. If evidence arrives at a later information stage, a proposition can become established without contradicting the earlier state of knowledge. The following two-stage example makes this distinction precise.
On the information order 0\leq1, let U hold only at stage 1. Its intuitionistic negation is empty. Thus U\vee\neg U=U, which omits stage 0. Stagewise Boolean labels \mathtt{False},\mathtt{True} do not form a natural decision. This temporal proposition retains its information-growth semantics. A fixed record and a later evidence view instead define two indexed queries, each of which may admit its own decision.
The complete source-to-model theorem must preserve those indices and the decision constructors. Its remaining obligations include universe closure, equality, certificate-preserving erasure, and runtime adequacy.
An execution branch needs a retained decision. A logical proof of “one alternative holds” can omit which alternative supplied the proof. Allowing execution to inspect that erased choice would make erasure change program behavior. The elimination restrictions prevent this.
Elimination from a proof in Prop into a computational type is restricted to singleton propositions: propositions whose eliminators reveal no runtime branch information. The class includes empty and unit propositions and proof-irrelevant identity proofs. It excludes ordinary disjunction, truncated existence, and subset-proof projections. In particular, there is no rule that case-analyzes a proof of P or Q to synthesize a value in Type_i.
G |- u : P or Q G, p:P |- c_P : C G, q:Q |- c_Q : C G |- C : Prop
------------------------------------------------------------- (Or-Elim-Prop)
G |- orElim(u, c_P, c_Q) : C
G |- A : Type_i G, x:A |- P(x) : Prop
---------------------------------------- (Subset-Form)
G |- {x : A | P(x)} : Type_i
G |- a : A G |- p : P(a)
------------------------------------------ (Subset-Intro)
G |- <a, p> : {x : A | P(x)}
G |- s : {x : A | P(x)}
----------------------- (Subset-Elim-1)
G |- pi_1(s) : A
G |- s : {x : A | P(x)}
------------------------------------ (Subset-Elim-2)
G |- pi_2(s) : P(pi_1(s))Subset types package a computational witness together with an erased compliance proof. They are the proof-irrelevant refinement layer for Lex: a term of type {x : A | P(x)} carries a runtime value of type A and a proof that the value satisfies P. This is the source-language analogue of the refinement discipline used by Op for compliance-carrying artifacts: the carrier survives execution, while the proof certifies the refinement and erases. The certificate-carrying [T]A of Section 4.6, IssuedAct, EvidenceRef, and rule permits live in Type. Their operational references survive proof erasure, including when the asserted interface A lies in Prop. Squashing their existence yields a logical proposition, not an execution credential.
G |- A : Type_i
------------------------- (Squash-Form)
G |- ||A|| : Prop
G |- a : A
------------------------- (Squash-Intro)
G |- |a| : ||A||
G |- u : ||A|| G |- C : Prop G, x:A |- c : C
-------------------------------------------------- (Squash-Elim)
G |- squashElim(u, x.c) : CThe squash type ||A|| forgets computational content while retaining mere inhabitation. It is useful for existence claims where the witness does not matter operationally; we write exists x : A. P(x) as shorthand for ||{x : A | P(x)}|| when the witness is irrelevant. Like disjunction, squash eliminates only into Prop.
The next result checks the intended separation of proofs and values. Its effect premise ensures that removing a proof cannot remove an operation. Its equality premise limits transport to cases whose erased computation remains defined. These restrictions explain the fragment named in the theorem.
Let erase(-) delete every subterm whose type is in Prop, project <a, p> to erase(a), and drop proof-only arguments from eliminators. Let Lex_erased be the sub-calculus obtained by removing the Prop sort and all constructors whose only outputs lie in Prop.
Theorem (Prop erasure, restricted fragment). If G |- e : A [rho], G |- A : Type_l, every erased Prop-sorted subderivation has empty computational effect row, and every occurrence of J has a Prop-sorted motive or a closed scrutinee reducing to refl, then erase(G) |-_{Lex_erased} erase(e) : erase(A) [rho].
Proof sketch. By induction on the typing derivation. Computational forms preserve their typing under erasure; proof constructors disappear; subset values erase to their first projection; and squash and disjunction eliminators remain inside Prop. A J with a Prop motive erases with its result. A closed J scrutinee reduces to refl, so the term reduces to its reflexive branch before erasure. The empty-effect premise prevents erasure from leaving an effect without a computation. General open equality transport into Type needs an explicit cast in the erased calculus and is not claimed here. \square
4.2 Terms
A term is an expression of the language. We first describe function application and binding, then the finite searches used in legal rules. Variables use de Bruijn indices: zero refers to the nearest enclosing binder, one to the next binder, and so on. This convention makes renaming independent of the chosen variable names.
Typing judgments carry an effect row. We write G |- e : A [rho] for “under context G, expression e has type A and its immediate evaluation requires effects within rho.” A function type separately records its latent call effects. Effect rows are discussed in Section 4.3; the introduction and elimination rules below thread them through every binding form.
Value and computation bindings. Ordinary bindings x:A contain values and have empty immediate lookup effects. A recursive computation binding f:A@rho instead records the budget of evaluating that computation. Looking up such a binding can execute it. Its budget therefore appears even inside a returned lambda.
x:A in G
-------------------------- (Value-Lookup)
G |- x : A [empty]f:A@rho in G
-------------------------- (Computation-Lookup)
G |- f : A [rho]Effectful computation bindings cannot occur in a type-formation premise that requires an empty row. Value bindings retain the ordinary dependent type rules. Both binding forms preserve latent rows inside their types.
A rule may require different evidence for each jurisdiction. The dependent function type Pi(x:A).B describes a function whose result type B may depend on its argument x. A lambda supplies its body. Application substitutes the supplied value into that result type. The extra row rho records operations that calling the function may perform.
Lambda abstraction and dependent function type (Pi):
G |- A : Type_i [empty] G, x:A |- B : Type_j [empty]
------------------------------------------------------- (Pi-Form)
G |- Pi(x : A) [rho]. B : Type_{max(i,j)} [empty]
G, x:A |- b : B [rho]
------------------------------------------ (Lam-Intro)
G |- lam(x : A). b : Pi(x : A) [rho]. B [empty]
G |- f : Pi(x : A) [rho_1]. B [rho_2] G |- v : A [empty], v a value
------------------------------------------------------------ (App)
G |- f v : B[v/x] [rho_1 ∪ rho_2]The Lex-specific content is the effect threading. Pi-Form attaches a latent effect row rho to the function type, so a compliance rule’s return type can vary by jurisdiction while its effect budget stays visible. Lam-Intro introduces the function purely; the body’s row rides on the Pi. App incurs the union of the Pi’s latent effects and the function-position’s effects. An effectful argument is evaluated through the dependent sequencing rule below.
Let binding:
G |- A : Type_i [empty] G |- v : A [empty], v a value G, x:A |- b : B [rho]
---------------------------------------------------------------------- (Let)
G |- let x : A := v in b : B[v/x] [rho]Let substitutes a value. An effectful initializer first returns the value on which the continuation depends.
Value-indexed execution.
A rule can obtain a jurisdiction from an authenticated response and then request evidence whose type depends on that jurisdiction. Evaluation must retain the returned jurisdiction when it returns the evidence. Otherwise the result loses the index that explains its type.
Write F_\rho A for a computation returning a value of type A, with effects contained in \rho. The judgment \Gamma\vdash e:A\,[\rho] abbreviates this computation judgment. Value formation, written \Gamma\vdash_v v:A, has a separate rule class. Types depend on values. A computation enters a type only through an explicitly defined value constructor, such as a thunk whose type records its effects. Evaluation never substitutes an outstanding oracle request for a value index.
Suppose \Gamma,x:A\vdash B(x):\mathrm{Type}_j is a pure family. Dependent sequencing has the following result type: \frac{\Gamma\vdash m:F_\rho A\qquad \Gamma,x:A\vdash k(x):F_\sigma B(x)} {\Gamma\vdash \operatorname{dbind}(m,x.k(x)): F_{\rho\cup\sigma}\bigl(\Sigma x:A.\,B(x)\bigr)}. Here \sigma bounds every permitted returned value’s continuation. The dependent pair contains the returned value and the corresponding result. If the result family is constant, ordinary sequencing may project the second component. A nonconstant family retains its first component or transfers that component into an enclosing dependent context.
This rule is constructed from ordinary sequencing: \operatorname{dbind}(m,k) = \operatorname{bind}\bigl(m,x. \operatorname{bind}(k(x),y.\operatorname{return}(x,y))\bigr). Effectful application first evaluates the function, then its argument, and then the function body. Its dependent elaboration is \operatorname{bind}(f,g.\operatorname{dbind}(a,x.g(x))). This retains the argument value when the result type depends on it. Effectful dependent matching does the same with its scrutinee. The pure App, Let, and Match-Dep rules apply inside these value-bound continuations. The elaborated source contains the dependent pair explicitly. An ordinary effectful let can return an unpaired result when its type is well formed in the outer context. This preserves the ordinary value returned by the source Let constructor.
Levy’s call-by-push-value separates values and computations. Vákár’s dependent extension identifies the additional conditions needed when a result type depends directly on a suspended computation (Levy 2006; Vákár 2016, Definition 4). The dependent-pair construction above uses ordinary sequencing. It does not assume those additional dependent Kleisli operations for arbitrary state or writer effects.
Proposition (dependent sequencing preserves the returned index). Let A be a value type and B:A\to\mathrm{Type} a pure family. Interpret computations by \operatorname{Return}(v), \operatorname{Refuse}(r), \operatorname{Emit}(e,c), and \operatorname{Await}(q,h). A request q has a declared response type R(q), and h takes a value of that type. Then every returned value of \operatorname{dbind}(m,k) has the form (a,b), where a:A is the value returned by m and b:B(a) is returned by k(a). The observed trace contains the first computation’s trace followed by the continuation’s trace. Refusal and suspension preserve the prefix already observed.
Proof. Define bind by structural recursion. A return invokes its continuation. A refusal propagates unchanged. An emitted event remains before the recursively bound computation. A request retains its response type and binds each response continuation. Applying these four clauses twice gives the displayed construction. Only the return clause introduces a pair, and that clause uses the same value a to select k(a) and construct its first component. Induction on a finite execution gives trace concatenation. The refusal and request clauses retain its prefix. \square
Regularity and substitution. In the family interpretation, a context is a set G, a type is a family A:G\to\mathrm{Type}, and a value is a section v:\prod_{g:G}A(g). A substitution s:H\to G reindexes both by composition. Consequently a substituted value inhabits the substituted family. Context extension is \Sigma g:G.\,A(g). A returned a:A(g) extends this context before the continuation’s family is instantiated. This establishes regularity and substitution for this family construction. Source typing requires its own formation argument, given next. Relating the source relation to this model and to an executable checker requires additional adequacy theorems.
Source types have types.
A type assigned to an expression must itself have a type. Otherwise conversion can replace a valid result type by syntax that has no meaning as a type. The formation argument must use the source rules that assign those types.
Write \Gamma\vdash_s t:T for the structural source judgment. Its rules cover variables, five sorts, dependent functions, lambda, application, annotation, let, defeasibility, finite match, and conversion. The five sort rules concern \mathrm{Type}_i, \mathrm{Prop}, \mathrm{Rule}_i, \mathrm{Time}_0, and \mathrm{Time}_1. These are fourteen typing constructors on the source term syntax. The match rule has a return type from the outer context, shifted into each branch. The dependent motive displayed later has its own typing and interpretation obligations. Function types retain their effect-row field. The judgment establishes type formation, while the computation judgments above also constrain execution effects.
Two operations underlie this check. Weakening adds an unused assumption while retaining an existing typing derivation. Substitution replaces a bound variable by a value of its declared type. Indices must move when a binder is inserted, or a variable could refer to the wrong assumption. The shift notation below records that move.
We make context storage explicit. Write \uparrow_k^d t for shifting the free indices at or above k by d. Extending a context by A stores \Gamma.A=(\uparrow_0^1 A):: \operatorname{map}(\uparrow_0^1)(\Gamma). The variable rule retrieves the stored type directly. A well-formed context starts with the empty context and extends only by a type already formed in its preceding context: \frac{}{\mathsf{wf}(\varnothing)}\qquad \frac{\mathsf{wf}(\Gamma)\qquad\Gamma\vdash_s A:\mathrm{Type}_i} {\mathsf{wf}(\Gamma.A)}. Each match branch has a telescope of binder types. Every binder type must form in the context containing the preceding binders.
Pure conversion. Let \longrightarrow_c be the compatible closure of beta reduction, let substitution, annotation erasure, and the following case rules. An empty exception list reduces to its base body. A leading wildcard branch returns its body without inspecting the scrutinee. A leading constructor branch fires after its constructor name and arity match. The leading branch can be skipped only after an observed constructor fails that name or arity test. A neutral scrutinee supplies no such observation. Nonempty exception lists retain their exception structure while their subterms can reduce. Execution selects the applicable exception under the priority rules of Section 4.4.
Define \equiv_c as the reflexive, symmetric, transitive closure of \longrightarrow_c. In particular, a neutral or suspended type is equal to itself. This definition supplies an equality relation without assuming normalization or a decision procedure for that equality. The source conversion rule is \frac{\Gamma\vdash_s e:A\qquad A\equiv_c B\qquad \Gamma\vdash_s B:\mathrm{Type}_i} {\Gamma\vdash_s e:B}. Its formation premise is essential. Annotation erasure gives \operatorname{Annot}(\mathrm{Type}_1,\operatorname{IntLit}(0)) \equiv_c\mathrm{Type}_1. Without target formation, conversion could assign that annotation as the type of \mathrm{Prop}. The integer annotation has no sort in this source core. The displayed conversion rule therefore rejects it while retaining conversion between formed types.
Theorem (Structural source substitution and regularity). For the fourteen source typing constructors above: \begin{align*} \Gamma\vdash_s t:T &\ \Longrightarrow\ \Gamma.A\vdash_s\uparrow_0^1t:\uparrow_0^1T,\\ \Gamma\vdash_s u:A,\quad\Gamma.A\vdash_s t:T &\ \Longrightarrow\ \Gamma\vdash_s t[u/0]:T[u/0],\\ \mathsf{wf}(\Gamma),\quad\Gamma\vdash_s t:T &\ \Longrightarrow\ \exists i.\ \Gamma\vdash_s T:\mathrm{Type}_i. \end{align*} The first clause is syntactic weakening. Its extended context is well formed when \Gamma is well formed and A is formed there.
Proof. Pure reduction commutes with shifting and substitution. The constructor case uses the simultaneous argument operation described below. The reflexive, symmetric, transitive closure inherits both compatibilities, so conversion also commutes with both operations.
Induct on the source typing derivation for weakening. Variable lookup uses the stored shifted type. Each binder increases the shift depth. Branch telescopes shift at successive depths, and their formation derivations shift with them. The conversion case transports both its equality and its target-formation derivation. The same induction proves typed substitution, using substitution composition under binders and the substitution law for conversion. All fourteen constructors retain their actual premises.
For regularity, induct on the typing derivation in a well-formed context. Lookup formation follows by induction on context generation and weakening. Sorts and function formation have their displayed universe levels. For a lambda, the body induction gives the codomain’s universe, which forms the dependent function type. For application, regularity of the function first gives formation of its function type. Inverting that formation gives \Gamma.A\vdash_s B:\mathrm{Type}_j. Typed substitution then forms B[u/0]. The let case uses the same argument on the body’s type. Annotation, defeasibility, match, and conversion carry a formed result type in their premises. These cases exhaust the source relation. \square
Application and let retain their dependent result rules. Formation of their substituted result is a conclusion of this argument. For example, (\lambda A:\mathrm{Type}_0.\,\lambda x:A.\,x)\, \mathrm{Time}_0 :\Pi x:\mathrm{Time}_0.\,\mathrm{Time}_0. The corresponding let expression has the same type. Open dependent contexts use the same substitution theorem.
Pure conversion and dependent products.
Beta preservation needs more than substitution. A lambda can acquire a different function type through conversion. Its domain and codomain must still agree with those used by application. Write \operatorname{Pi}(A,\rho,B) for the source function-type constructor, with stored effect-row field \rho. Equality of these fields includes their presence or absence.
Theorem (Pure source confluence and product compatibility). Any two finite \longrightarrow_c reductions from one term have a common reduct. Moreover, \operatorname{Pi}(A,\rho,B)\equiv_c \operatorname{Pi}(A',\rho',B') \quad\Longrightarrow\quad \rho=\rho',\quad A\equiv_c A',\quad B\equiv_c B'. Both statements concern the pure relation of Section 4.2 on source syntax.
Proof. Parallel contraction reduces compatible subterms together. The complete-development triangle states that every parallel reduct of t contracts in parallel to its complete development. Its mutual proof covers terms, argument lists, branches, and exceptions. The binder cases use parallel substitution and simultaneous argument instantiation. Pure steps embed into parallel contraction, and each parallel contraction expands into finitely many pure steps. The triangle therefore proves confluence of \longrightarrow_c^*.
A finite conversion zigzag has a common reduct by confluence. Reduction from a function-type constructor preserves that constructor and its stored row. Its domain and codomain reduce componentwise. Applying this observation to the common reduct proves the displayed decomposition. \square
The statements are source_steps_confluent and pi_convertible_decomposition in ProductCompatibility.v. They supply product compatibility to beta_preservation in BetaPreservation.v. Pure confluence does not assert termination or confluence of the wider symbolic execution relation.
Preservation along source reductions.
A reduction below a binder must preserve typing in the binder’s local context. For example, the following two beta steps occur below the outer lambda: \begin{align*} &\lambda A:\mathrm{Type}_0.\, ((\lambda B:\mathrm{Type}_0.\, ((\lambda C:\mathrm{Type}_0.\,C)\,B))\,\mathrm{Time}_0)\\ &\quad\longrightarrow_b \lambda A:\mathrm{Type}_0.\, ((\lambda B:\mathrm{Type}_0.\,B)\,\mathrm{Time}_0)\\ &\quad\longrightarrow_b \lambda A:\mathrm{Type}_0.\,\mathrm{Time}_0 . \end{align*} Each term has the same assigned type \Pi A:\mathrm{Type}_0.\,\mathrm{Type}_0. The first contraction also lies below the inner lambda and inside an application’s function position.
We now define the relation used in this example. Abbreviate the source constructors Defeasible and Match by D and M. Write E for an exception list and L for a branch list. The branches *\Rightarrow b and c[n]\Rightarrow b denote a wildcard and a constructor pattern with name c and n binders.
The source value predicate V_b holds on sorts, variables, constants, literals, axiom-use nodes, lambdas, and function-type constructors. It also holds on data introductions whose arguments all satisfy V_b. Here literals are integer, rational, or string literals. This predicate tests syntax and does not assert normality. The Boolean H(s,c,n) is true exactly when s is a data introduction with name c and n arguments.
Define \longrightarrow_b by seven head rules: \begin{align*} (\lambda x:A.\,b)\,a &\longrightarrow_b b[a/x],\\ \operatorname{let}\ x:A=v\ \operatorname{in}\ b &\longrightarrow_b b[v/x],\\ \operatorname{Annot}(e,A) &\longrightarrow_b e,\\ D(A,b,[]) &\longrightarrow_b b,\\ D(A,b,e::E) &\longrightarrow_b D(A,b,E),\\ M(s,R,(*\Rightarrow b)::L) &\longrightarrow_b b,\\ M(s,R,(c[n]\Rightarrow b)::L) &\longrightarrow_b M(s,R,L). \end{align*} The wildcard rule requires V_b(s). The final rule requires V_b(s), H(s,c,n)=\mathrm{false}, and L\ne[]. Beta and let substitution have no value premise.
Close these rules under exactly seven context forms: \begin{gather*} [-]\,a,\qquad \operatorname{Annot}([-],A),\qquad \lambda x:A.\,[-],\\ \operatorname{let}\ x:A=v\ \operatorname{in}\ [-],\qquad D(A,[-],E),\qquad M([-],R,L),\qquad \operatorname{Pi}(A,\rho,[-]). \end{gather*} For each form, t\longrightarrow_b u implies C[t]\longrightarrow_b C[u]. Every recursive premise uses \longrightarrow_b itself. Thus beta may occur at arbitrary finite depth within these contexts. These seven heads and seven context rules are the fourteen constructors of step in BetaTracePreservation.v. They contain no typing premise. Write \longrightarrow_b^* for their reflexive-transitive closure.
Theorem (Source trace preservation). For every context \Gamma, source terms t,u, and assigned type T, \mathsf{wf}(\Gamma),\qquad \Gamma\vdash_s t:T,\qquad t\longrightarrow_b^*u \quad\Longrightarrow\quad \Gamma\vdash_s u:T. The context formation is the generated judgment of Section 4.2. The assigned type T is arbitrary, including types obtained through outer conversion. The conclusion retains that exact type. Every such trace also belongs to Repaired.steps in RepairedReduction.v.
Proof. Induct on one restricted step, generalizing the context and assigned type. Product compatibility converts the beta argument to the lambda’s domain. Typed substitution produces the reduct and transports codomain conversion. Source regularity forms the original assigned type, permitting the final conversion. These steps constitute BetaPreservation.v. Let substitution uses the source substitution theorem. Typing generation through outer conversion proves the other five head cases. The seven context cases use their typing compatibility lemmas.
For lambda bodies, let bodies, and product codomains, recover domain formation from the enclosing typing derivation, including its outer conversions. The context-formation rule then constructs \mathsf{wf}(\Gamma.A) before the induction hypothesis is used there. The other four contexts retain \Gamma. Induction on finite traces preserves the assigned type at every step. Each rule is also a rule of Repaired.step, so induction gives the claimed trace inclusion. \square
The theorem is trace_preservation; its operational inclusion is captured_steps. The theorem typed_captured_trace bundles both conclusions. The subrelation obtained by omitting beta has six head rules and seven recursive contexts. Its preservation theorem in AdministrativeReduction.v needs no context-formation premise. Its steps and finite traces embed into the relation above.
The examples in Examples.v retain the displayed two-step trace at both its function type and the formed convertible target \operatorname{Annot}\bigl( \operatorname{Pi}(\mathrm{Type}_0,\mathrm{None},\mathrm{Type}_0), \mathrm{Type}_1\bigr). They also prove beta preservation below dependent declarations A:\mathrm{Type}_0,\ x:A, and within let bodies and product codomains.
Exception peeling removes the leading entry without testing its guard or priority. Its type-preservation proof establishes no lawful exception selection. The pure relation \longrightarrow_c retains nonempty exception lists. The relation \longrightarrow_b is also distinct from Section 4.3’s labelled runtime, which treats lambdas as values.
Application arguments and constructor firing remain outside this theorem. So do domain and type-field reductions, let initializers, match return types and branches, and exception guards and bodies. Pairs, projections, dependent pairs, recursion, sanctions, defeat elimination, temporal and modal forms, holes, principle balancing, and unlocking add no reduction rules here.
These results concern the structural source judgment and the stated reduction relations. Constructor signatures must still justify match binders and exhaustive coverage. Full operational preservation must also cover the remaining execution rules. Progress asks whether a closed well-typed program is already a value or has an allowed next step. For effectful evaluation the allowed outcomes also include an explicit request or refusal. Confluence asks whether two reduction paths from the same expression can reach expressions that both reduce to a common expression. Normalization, effect soundness, and the source-to-checker relation retain their separate statements. The richer dependent motive, modal operators, certificates, and execution outcomes require the additional interpretation clauses described below.
Authenticated resumption. A suspended request binds the source program, environment, authority contract, response family, and returned indices. Authentication establishes a response for that exact request. Value validation then checks membership in its response fiber. For example, after an officer returns n=2, a request for \mathrm{Vec}(\mathrm{Nat},2) accepts a two-entry response. A valid signature on three entries still fails that request. A closure can generate the dependent request for each returned n, so the construction supports higher-order effectful continuations.
Dependent sequencing retained both a jurisdiction and its evidence. The dependent pair type formalizes that package. Its first component selects the type of its second component. A projection retrieves a component while preserving this dependence.
Dependent pair type (Sigma) and projections:
G |- A : Type_i [empty] G, x:A |- B : Type_j [empty]
------------------------------------------------------- (Sigma-Form)
G |- Sigma(x : A). B : Type_{max(i,j)} [empty]A Sigma type packages, for example, a jurisdiction together with jurisdiction-specific evidence.
Quantification over finite legal collections:
The Pi-form above is the general dependent function space of type theory. It is not the surface form for legal quantification over a company’s finite rosters of directors, shareholders, officers, or beneficial owners. Lex therefore adds separate bounded quantifiers ranging over explicit finite collections.
A finite bound limits the variables being quantified. Executable decision also needs an effective enumeration and a decision procedure for each instantiated predicate. The enumeration states its domain and evidence view. A roster observation covers that supplied roster. A rule about every legally relevant director also needs admitted evidence that the roster covers that legal domain.
The runtime separates finite search from evidence acquisition. A truncated ownership search returns inspected nodes, unresolved frontiers, and a view identifier. Further evidence can resume it. A rule requiring an authorized judgment uses a typed discretion hole. An incomplete search establishes neither a negative legal decision nor a need for discretion. A negative decision requires complete domain coverage and a refutation for every candidate. Positive evidence can establish an existential before the remaining search finishes.
These graphs use different composition laws for different edges. An equity edge carries a fraction and multiplies along a path, so a 60% holder of a 60% holder controls 36%. A board-control edge composes transitively rather than multiplicatively: under most statutes, a party with board control of an entity that controls another entity controls the second entity outright. A contractual edge may confer only a veto over specified acts.
A traversal that treats the graph as homogeneous therefore computes a number that answers no legal question. Either it multiplies through control edges, understating who controls what, or it treats equity edges as transitive, overstating it. The graph must be typed by edge kind and the composition rule chosen per kind, and where a jurisdiction’s own definition of control differs — as they routinely do on thresholds and on whether de facto control counts — the rule belongs in that jurisdiction’s pack rather than in the traversal.
Effective finite domains. A FiniteDomain(A) carries an ordered vector items : Vec(n,A), admitted decidable equality, and a proof that its entries are distinct. Membership means equality to an entry. Its order and values are immutable query inputs. Lists and multisets remain ordinary data. Conversion to a finite domain removes repeated values through the declared equality. Occurrence counts use the original collection explicitly.
The notation Collection(A) below supplies such a domain for executable value quantification. An effectful producer first binds the domain as a value. Logical finite quantification forms the displayed conjunction or disjunction. Executing its decision requires the predicate interface below.
G |- C : Collection(A) [rho_C] G, x:A |- P(x) : Prop [rho_P]
----------------------------------------------------------- (Forall-Bounded)
G |- forall x : A in C. P(x) : Prop [rho_C ∪ rho_P]G |- C : Collection(A) [rho_C] G, x:A |- P(x) : Prop [rho_P]
----------------------------------------------------------- (Exists-Bounded)
G |- exists x : A in C. P(x) : Prop [rho_C ∪ rho_P]G |- C : Collection(A) [rho_C] G, x:A |- P(x) : Prop [rho_P]
----------------------------------------------------- (ExistsUnique-Bounded)
G |- exists! x : A in C. P(x) : Prop [rho_C ∪ rho_P]Operationally, if enum(C) = [c_1, ..., c_n], then forall x : A in C. P(x) reduces to P(c_1) ∧ ... ∧ P(c_n) and exists x : A in C. P(x) reduces to P(c_1) ∨ ... ∨ P(c_n). The empty conjunction is top; the empty disjunction is bottom. Unique existence expands to existence plus a uniqueness side condition:
exists! x : A in C. P(x) reduces to (exists x : A in C. P(x)) ∧ ∧_{i,j} ((P(c_i) ∧ P(c_j)) -> c_i = c_j).
This is the quantificational shape that statutes use when they say “every director shall …”, “some shareholder may …”, or “the company shall have exactly one secretary.”
A TotalDecision(C,P) supplies a total pure decision for every member, with correctness and termination evidence and an execution bound. Its result is Yes(p) or No(n), where p:P(x) and n:P(x) -> bottom_prop. A bare Boolean supplies neither proof. The pure admissible fragment uses these total interfaces. The runtime also accepts effectful decision producers. Their latent rows and query indices remain in each suspended continuation.
Bounded existential quantification supports witness extraction:
C is a supplied collection value or value-bound variable
G |- C : Collection(A) [rho_C]
G |- h : exists x : A in C. P(x) [rho_h]
G |- dec : Pi(x : A)[rho_call]. Dec(P(x)) [rho_dec]
---------------------------------------------------------- (Choose)
G |- choose(C,h,dec) : Witness(A,C,P)
[rho_C union rho_h union rho_dec union rho_call]Here Witness(A, C, P) is a certificate type in the prelude, the shared signature of declared data and evidence types, with constructor Found(a, m, p) where a : A, m : Member(a, C), and p : P(a). The caller supplies C as runtime data. A producer with effects first binds its collection through Let, which charges those effects. The proof and decision procedure refer to that same collection value. The decision procedure scans it and returns the first positive branch. Its latent call row is charged on every call. Set union records event kinds, so repeated calls do not require a larger set. A pure lambda with an oracle body still contributes its latent oracle row. The proof h establishes that this scan cannot fail; it is not destructured into computational data. The same procedure maps each bounded quantifier to a Boolean fold. That Boolean, rather than a proof in Prop, is what executable rules consume. Under unique existence, returned witnesses have propositionally equal values by the uniqueness proof. A fixed enumeration and deterministic decision procedure also select the same first index. This does not turn propositional equality into definitional equality.
Some legal rules quantify over rules rather than over entity data. For that purpose the full calculus reserves a higher-order meta-quantifier:
Pi_meta : (Rule_l -> Prop) -> Prop
It expresses meta-rules such as “every rule granting privilege X must also impose constraint Y.” This constructor is outside the admissible fragment: its domain is the open-ended rule space rather than an explicit finite collection, so checking it requires reflection over rule syntax and metadata rather than bounded iteration over enumerated data.
Proposition (effective finite decision and choice). Let C be an effective finite domain with n distinct entries. Assume TotalDecision(C,P). Bounded universal, existential, and unique existential propositions have total decision procedures. Given a proof h of bounded existence, choose(C,h,dec) returns a member and a proof of its predicate. Each procedure uses at most n predicate calls after domain admission.
Proof. Scan the ordered vector. Universal search returns the first refutation or combines all positive proofs. Existential search returns the first positive witness or combines all refutations. Unique search counts distinct positive entries. Exactly one yields existence and uniqueness. Zero or two distinct positives refute unique existence. Enumeration completeness justifies the case analysis for any purported member. Termination follows from the finite scan and each call’s bound. For choose, all-negative results would contradict h. The runtime obtains its value from a positive decision, without eliminating an erased existence proof into data. For an empty domain, universal search returns true and both existential searches return false. \square
The previous search finds one witness. A rule may instead require a witness for every member of a finite roster. Running that search once per member constructs a table assigning each input its witness. Bounded Skolemization names this passage from finite existential claims to a witness function.
Proposition (constructive finite choice; bounded Skolemization). Let C and D be effective domains of sizes n,m. Assume a total pure admitted decision for each P(x,y), with the arguments and evidence view fixed, and h:\ \forall x\in C.\ \exists y\in D.\ P(x,y). An executable table defines f:\operatorname{Element}(C)\to\operatorname{Element}(D) and proves P(x,f(x)) for every member. It uses at most nm predicate calls.
Proof. Specialize h for each ordered entry within Prop. Run finite choice on D with that proof and the supplied decision procedure. Store the first positive index and its proof. Decidable domain equality gives terminating lookup. The stored witness supplies the output and establishes its predicate. The existence proofs exclude unsuccessful rows. If C is empty, the empty table is the required function, including when D is empty. Row uniqueness makes all satisfying functions pointwise propositionally equal. \square
Resumable finite search. An external predicate request returns Yes(p), No(n), Await(k), or a typed operational error. A timeout supplies no refutation. The continuation binds the domain, predicate, values, view, completed results, remaining requests, and effect budget. Resumption uses those indices. A changed view creates a new indexed evaluation and preserves the earlier receipt.
Existential search can return a witness immediately. Universal search can return a refutation immediately. Their opposite answers require all decisions. Unique existence requires one positive and negative decisions for every other distinct entry. Two distinct positives refute it immediately. Otherwise unresolved entries retain Await. Once the necessary decisions arrive, the search constructs its certificate automatically. The total-decision theorem concerns the pure completed interface. The general runtime retains effectful and suspended searches with the budgets of Choose.
Worked examples. The Seychelles International Business Companies Act 2016, s.130(1), “A company shall at all times have at least one director appointed in accordance with this Act” (the section closes with a cross-reference to other written law of Seychelles), is a bounded existential over the directors collection:
exists d : Director in c.directors. AppointedUnderAct(d)The predicate is appointment, not personhood. Section 130(1) states its test as appointment under the Act, and s.133(1) provides that a director shall be an individual or a body corporate, so a natural-person guard would encode a requirement this statute does not impose.
Threshold statutes are the same finite-collection discipline expressed through cardinality. The Companies Act 2006, s.154 requirement that a public company have at least two directors is:
|c.directors| >= 2and, when a jurisdiction counts only directors satisfying a predicate, the same operator appears as a filtered cardinality:
|filter NaturalPerson c.directors| >= 2Pattern matching selects a branch from an observed constructor. Its result type may also depend on that observation. For example, a jurisdiction constructor can select the corresponding evidence type. The motive P below states this dependence before the branches are checked.
Pattern matching (dependent):
G |- v : T [empty], v a value G, x:T |- P : S [empty] S in {Prop, Type_k}
if G |- T : Prop and S = Type_k, then SingletonProp(T)
(for each branch C_i xs => b_i, where C_i : Pi(xs : Args_i). T:
G, xs : Args_i |- b_i : P[C_i(xs)/x] [rho_i])
-------------------------------------------------------------- (Match-Dep)
G |- match v return x. P with | C_1 xs_1 => b_1 | ... : P[v/x] [⋃_i rho_i]The dependent motive lets the cross-jurisdictional rule in Section 7.2 return a result type Pi(_ : EntityContext j). ComplianceVerdict that varies with the jurisdiction j. When the scrutinee itself lives in Prop, the side-condition from the Prop sort section applies: elimination into Type_k is admitted only for singleton propositions, so disjunction and squash proofs cannot be case-analyzed to produce runtime data. In the admissible fragment (Section 5), match is restricted to non-dependent motives over prelude constructor types with known finite variants. Effectful scrutinees use value-indexed sequencing, which joins their effects with every branch’s effects.
Match binders and substitution. The structural source rule types each branch body against \uparrow_0^n R, where R is the outer return type and n is the branch arity. Its binder types form sequentially in the preceding branch context. Generalized weakening transports these formation derivations as well as the branch body. The return type’s initial shift accounts for the new branch variables. This proves weakening for the whole structural source relation, including its match case.
Constructor arguments require a corresponding simultaneous operation. Write \operatorname{inst}(\vec a,b) for opening a branch body b with the n arguments \vec a in source order. The rightmost argument replaces index zero. Each insertion protects its free variables while the remaining binders are removed. Equivalently, reverse the argument list, shift each argument by the number of later substitutions, and substitute those protected arguments successively. This construction retains open argument dependencies.
For every cutoff k, shift amount d, and replacement u, \begin{align*} \uparrow_k^d\operatorname{inst}(\vec a,b) &=\operatorname{inst}\bigl( \operatorname{map}(\uparrow_k^d)\vec a, \uparrow_{k+n}^d b\bigr),\\ \operatorname{inst}(\vec a,b)[u/k] &=\operatorname{inst}\bigl( \operatorname{map}([u/k])\vec a, b[\uparrow_0^n u/(k+n)]\bigr). \end{align*} These are equalities of source syntax. Induction over the protected argument list proves them using shift and substitution composition. For example, \operatorname{inst}((\operatorname{Var}0,\operatorname{Var}1), \operatorname{Var}1)=\operatorname{Var}0, \qquad \operatorname{inst}((\operatorname{Var}0,\operatorname{Var}1), \operatorname{Var}0)=\operatorname{Var}1. An unprotected succession can capture the first inserted variable during the next substitution. The simultaneous operation preserves both open arguments. Its laws establish shift and substitution compatibility of pure constructor reduction and hence of \equiv_c.
Constructor-signature correctness supplies a further obligation. The constructor’s declared argument telescope must match the branch’s telescope, and a coverage result must justify elimination on every admitted scrutinee. Structural regularity alone does not prove those execution properties or dependent-motive preservation.
Type annotation:
G |- A : Type_i [empty] G |- e : A [rho]
------------------------------------------ (Annot)
G |- (e : A) : A [rho]An annotation is a machine-checkable assertion that e has type A; the effect row is preserved unchanged.
A computation can call itself, including from a function it returns. Its effect declaration must account for those later calls. The following rule assigns the recursive reference its declared budget on every use. It permits nontermination, which the finite admissible fragment excludes.
Budgeted recursion:
G, f:A@rho |- b : A [sigma] sigma subseteq rho
--------------------------------------------------- (Rec)
G |- fix f : A [rho] := b : A [rho]The binding is a computation, not an already evaluated value. Computation-Lookup charges rho whenever the body uses f. A lambda capturing that use includes the budget in its latent row. Runtime unfolding substitutes the same fixpoint for the budgeted binding:
fix f : A [rho] := b --> b[(fix f : A [rho] := b)/f]Budgeted recursive substitution. If G,f:A@rho |- e : B [sigma] and G |- t : A [tau] with tau subseteq rho, then substitution for f preserves the derivation at the original budget sigma, with the corresponding type substitution. In the lookup case, weaken tau to the already charged rho. In the lambda case, the induction preserves the body’s row and therefore its complete latent function type. Binding, application, and bridge cases retain their declared latent rows. This lemma is separate from substitution of pure values. The empty-row restriction on type formation prevents an effectful computation from becoming a supposedly pure type index.
For example, a fixpoint that calls an oracle before returning a lambda cannot type that lambda as latent-pure when it invokes the fixpoint again. Its recursive lookup contributes the oracle budget to the lambda body. Declaring the actual latent row admits that recursive program and accounts for every repeated invocation.
Rec retains general recursion and can diverge. Its effect result bounds every finite execution prefix. The admissible fragment continues to exclude recursion while its normalization theorem is open.
4.3 The Effect System
A date comparison, a request for judgment, and a registry update perform different operations. An effect row records the kinds of operations that evaluation may perform. Lex uses a finite set drawn from the following vocabulary:
| Effect | Meaning |
|---|---|
read |
Pure observation of state |
write(scope) |
Mutation within a named scope |
attest(authority) |
Assertion under an authority |
authority(ref) |
Exercise of an authority role |
oracle(ref) |
Query to an external oracle |
sanctions_query |
Distinguished sanctions check |
discretion(authority) |
Exercise of discretionary judgment |
unsettled(dom) |
Suspension on unsettled law in domain dom |
Effect rows form a bounded semilattice under join (+), with the empty row as unit. The ordering is by subsumption: row a is subsumed by row b when every effect in a is also in b. Effect weakening enlarges an expression’s immediate budget while preserving its type, including any latent row inside that type.
G |- e : A [rho_1] rho_1 subseteq rho_2
------------------------------------------- (Effect-Weaken)
G |- e : A [rho_2]Constructing or storing a function does not perform its latent effects. Calling a function that queries sanctions requires that effect at the application site. Weakening the immediate row cannot remove or alter the latent row.
The sanctions_query effect is distinguished: the type checker tracks its presence to trigger additional compliance obligations at the call site.
Composition is the semilattice join effect_join(rho_1, rho_2) = rho_1 union rho_2: commutative, associative, idempotent, with the empty row as unit.
A row counts effect kinds, rather than occurrences. A function called twice can emit two oracle events while retaining one oracle entry in its row. Ordering and repeated events remain in the execution trace.
Immediate and latent effects. A lambda is a value. Its body can require effects although constructing the lambda requires none. For example, a body with row {oracle(ref)} gives a lambda with immediate row empty and that latent row in its Pi type. App includes the latent row when the function is called. The body’s row is therefore not bounded by the lambda’s immediate row.
Define an immediate subderivation on the actual Lex typing derivation. Follow term-premise edges except the edge from Lam-Intro to its unevaluated body. Type-formation premises have empty rows. Application includes its function and argument premises. Let, bounded quantifiers, match, defeasible rules, annotation, and recursion include the term premises displayed in their rules. Modal rules include their term premises and stated local effects. Weakening includes its original derivation. Take the reflexive transitive closure of these edges.
Proposition (immediate-subderivation bound). If a derivation of G |- e : A [rho] has an immediate subderivation with row rho’, then rho’ subseteq rho.
Proof. Inspect the actual typing rule at each permitted edge. Its conclusion either preserves the premise row, includes it in a union, or enlarges it by Effect-Weaken. The lambda-body edge is absent. Transitivity proves containment along every permitted path. This proof does not change the conclusion row of Lam-Intro. \square
Application exposure. If f has latent row rho_latent, immediate row rho_f, and argument a has row rho_a, then App assigns their union. A returned function retains its own latent row in the result type. Its later application exposes that row through the same rule.
Runtime relation. Write S; e --alpha--> S’; e’ for one runtime step, where alpha is a finite list of effect events. State S contains typed value and computation bindings, the store, admitted authority records, evidence views, and suspended continuations. The relation uses the actual Lex constructors and typing rules. Its evaluation contexts select the function before the argument, the initializer before a let body, and the scrutinee before a match branch. Choose uses the supplied collection value, evaluates its decision function, and charges each call’s latent row. Bounded predicates use the admitted enumeration. Defeasible evaluation visits the base, each guard, and each satisfied exception body in source order. Priority then selects the result. An annotation evaluates its term. Modal operations evaluate their arguments before checking the corresponding authority operation. There is no runtime context beneath an unevaluated lambda.
The administrative rules emit the empty event list. Beta substitutes a value into the body. Let and match substitute evaluated values. Recursion uses its budgeted computation binding and the distinct substitution lemma above. A primitive’s declared signature gives its result type and local effect row. Its transition preserves the complete store typing. New locations extend that typing consistently. Existing locations, closures, capability references, and authority records retain their declared types and exact indices.
A returned value has its full declared type, including every latent function and bridge row. A suspended continuation retains a typed captured environment, result type, remaining effect budget, evidence references, and resumption point. Its budget stays within the current expression’s budget. Serialization and resumption preserve these data. The transition emits only events named in its local row. Authority issuance, rule use, recognition, and adoption also satisfy Section 4.6. A failed or pending protected check returns a typed outcome or suspends before the protected effect. Resumption rechecks current authority. Symbolic reduction beneath binders remains a separate relation.
Primitive contracts connect declared effects to external behavior. The next theorem carries those local guarantees through evaluation contexts, stored values, and suspended continuations. It bounds each finite execution prefix, including one that later suspends.
Theorem (runtime effect containment). Suppose the initial state is well typed, G |- e : A [rho], and each primitive transition satisfies its full value, store, continuation, and effect contract. Then every event in every finite runtime prefix from S; e belongs to rho. This statement permits divergence and suspension. It bounds executed effects rather than promising termination.
Proof outline over Lex typing. First prove substitution for a well-typed value with empty immediate row. The substituted value keeps its complete type, including every latent Pi row. Induct on the actual typing derivation, using binder lifting and the existing conversion obligations for dependent types. Prove budgeted computation substitution separately, using Computation-Lookup rather than pure-value lookup. That lemma preserves the latent rows of closures capturing recursion. Next prove the context lemma: each runtime evaluation context includes the selected term’s budget in its conclusion budget. The lambda-body case is absent by construction. For beta, the application’s budget contains the body budget through App; value substitution preserves it. Let, match, bounded quantifiers, and defeasible selection use their displayed unions. Choose includes its collection, proof, decision evaluation, and latent call budgets. Recursion uses the budgeted substitution lemma with the fixpoint’s declared row. Modal cases retain their local and latent bridge rows. Primitive cases preserve store typing, full returned-value types, and typed suspended continuations under their transition contracts. Thus each step emits events within the current budget and preserves the complete configuration typing at a budget contained in it. Induction over the runtime prefix proves the result. The proof requires no generic row-tree projection.
Direct-term runtime fragment. The module ActualEffects.v defines a separate call-by-value relation on Lex.Syntax.Term. Its typing judgment carries runtime value shapes and latent effect rows. It covers variables, sorts, constants, Pi, lambda, application, let, annotation, match, and defeasible rules. Constructor signatures determine the types of match bindings.
For this fragment, evaluation preserves value shapes and bounds every finite event prefix. A closure retains its typed environment and latent row. The same closure can be called twice, producing two effect events. An empty latent row cannot type a closure whose body calls an oracle. These results follow by induction on the term-indexed evaluation relation under explicit global and primitive contracts.
ActualState.v adds typed stores and primitive call records. Its forgetting relation connects stateful evaluation to that runtime fragment. Primitive contracts preserve cell types, declared frames, returned function rows, and recorded write effects. Typed let-bound host suspensions retain their environment, view, store, and remaining budget. Resumption uses the saved continuation and consumes its ticket. The stateful example returns an effectful closure, suspends, and later calls that closure without repeating its earlier write.
These results concern runtime representations. Dependent conversion, indexed row substitution, the remaining constructors, and general serialized continuations require further relations. The captured Coq effect type retains event kinds while omitting authority and scope indices. Exact authority and resource guarantees therefore remain separate obligations. The generic-tree theorem PaperMechanization.v/effect_monotonicity supplies a distinct support lemma.
Filling replaces a hole with checked evidence and retypes the result. The original hole is not a subderivation of the resulting term. Immediate and latent rows in that result remain subject to the same rules. A reusable authenticated rule can compute derived evidence without introducing a new signature for every intermediate value.
4.4 Defeasible Rules
The typing rule for a defeasible rule requires type agreement between the base and all exceptions, Boolean guards, and an effect-row join across base, guards, and exception bodies:
G |- A : Type_i G |- b : A [rho_0]
for each exception (guard_k, body_k, priority_k):
G |- guard_k : Bool [sigma_k] G |- body_k : A [rho_k] priority_k : Nat
--------------------------------------------------------------- (Defeasible)
G |- defeasible b unless (guard_1 => body_1 [p_1] | ... | guard_n => body_n [p_n])
: A [rho_0 ∪ ⋃_k (sigma_k ∪ rho_k)]Defeasible says: a defeasible rule has a base conclusion b and zero or more exceptions, each with a guard, an overriding body, and a priority. Three constraints hold simultaneously. Every exception body must inhabit the same type as the base body. Every guard must be of type Bool: guards are predicates evaluated to true or false, not arbitrary terms. Priorities are natural numbers and participate in the evaluation strategy, not the typing derivation.
The effect row of a defeasible rule is the union of the base body’s effects, every guard’s effects, and every exception body’s effects. Runtime evaluation visits every satisfied exception body, then selects the highest-priority result. Its static annotation retains the full union. An exception-only effect therefore cannot appear pure.
A lower-priority firing exception can therefore perform an effect even when another exception supplies the final value. defeasible_effect_join closes this rule-level equality in Rocq.
The elimination form defeat(r) returns the result selected by this evaluation. Priority selects the result after the source-order evaluation.
A priority graph is a finite directed graph whose nodes are pairs (principle, case_category). Write Reaches(x,y) for the reflexive-transitive closure of its edge relation. The graph is acyclic when no edge x -> y has Reaches(y,x). A rule set is well formed only when its graph is acyclic; principle_balancing_terminates decides this finite property. PrincipleBalance selects a firing exception only when no distinct firing exception reaches it. Edges point from a preferred principle to a defeated principle. The numeric priorities above are the linear instance: a strictly descending priority list is an acyclic chain. Thus the list evaluator is the decisive construction used here, while the graph records partially ordered principles without forcing unrelated cases into one numeric scale.
4.5 Temporal Modals
Lex has two temporal layers: first-class temporal objects and propositions about them. The objects carry effective dates, pack versions, rewrites, repeals, and derived deadlines. The propositions state when facts and obligations hold.
G |- r : RuleRef G |- t0 : Time_0
------------------------------------ (EffectiveDate)
G |- EffectiveDate(r, t0) : Time_0
G |- r : RuleRef G |- P : PackType G |- te : Time_0
--------------------------------------------------- (Active-Form)
G |- Active(r, P, te) : Prop
G |- r : RuleRef G |- P : PackType G |- te : Time_0
r in P.rules G |- d : EffectiveDate(r) <= te
G |- nr : not_repealed(r, P, te)
------------------------------------------------------ (Rule-Active)
G |- active(r, P, te, d, nr) : Active(r, P, te)
G |- id : PackId G |- version : PackVersion
G |- rules : Set Rule G |- repeals : Set (RuleRef x Time_0)
G |- effective_date : Time_0
---------------------------------------------------------------- (Pack)
G |- Pack(id, version, rules, repeals, effective_date) : PackTypeG |- P_old : PackType G |- P_new : PackType
G |- pc : conserves_or_repeals(P_old, P_new)
G |- pt : preserves_survivor_types(P_old, P_new)
G |- pd : P_old.effective_date <= P_new.effective_date
G |- rp : ReplayWitness(P_old, P_new)
------------------------------------------------------------------ (Rewrite)
G |- Rewrite(P_old -> P_new; pc, pt, pd, rp) : RewriteWitnessG |- P_old : PackType G |- P_new : PackType
-------------------------------------------------- (ReplayWitness-Form)
G |- ReplayWitness(P_old, P_new) : Type_0
G |- rule_ref : RuleRef
----------------------- (Repeal)
G |- Repeal(rule_ref) : RepealWitness
G |- rule_ref : RuleRef G |- trep : Time_0
--------------------------------------------------------- (Repeal-Effective)
G |- EffectiveDate(Repeal(rule_ref), trep) : Time_0
G |- r : RuleRef G |- P : PackType G |- te : Time_0
G |- pi : Active(r, P, te)
---------------------------------------------------------- (Eval-Rule)
G |- eval(r, P, te) : ComplianceVerdictEffectiveDate gives a rule a threshold in frozen historical time. Active-Form forms the activity proposition. Rule-Active constructs its proof only when the rule is present, effective, and not repealed. Here not_repealed(r,P,te) means te < t_rep for every tombstone (r,t_rep) in P.repeals. Pack includes rules and repeal tombstones. Rewrite takes proofs of all four pack-evolution obligations and is the sole constructor of RewriteWitness. Eval-Rule consumes an activity proof. A tombstone preserves prior derivations while blocking fresh activity proofs at and after its date. An evaluator whose pack omits the tombstone is stale.
Pointwise temporal modalities:
G |- t : Time_i G |- A : Prop
-------------------------------- (At)
G |- @t A : Prop
G |- t : Time_i G |- A : Prop
-------------------------------- (Eventually)
G |- diamond t A : Prop
G |- t1 : Time_i G |- t2 : Time_i G |- A : Prop
----------------------------------------------------- (Eventually-Interval)
G |- diamond[t1, t2] A : Prop
G |- t1 : Time_i G |- t2 : Time_i G |- A : Prop
----------------------------------------------------- (Always)
G |- box[t1, t2] A : Prop@t A asserts that A holds at time t. diamond t A asserts that A holds at some point after t; this form has no upper endpoint. The bounded form diamond[t1,t2] A requires a witness time u\in[t1,t2] at which A holds. box[t1, t2] A asserts that A holds throughout the interval [t1, t2].
The temporal rewrites:
G |- t : Time_0
------------------- (Lift)
G |- lift_0(t) : Time_1
G |- t : Time_0 G |- w : DerivationWitness(P)
------------------------------------------------ (Derive)
G |- derive_1(t, P, w) : Time_1
G |- d : Time_1 G |- delta : QualifiedExclusion(d)
--------------------------------------------------- (Toll)
G |- Toll(d, delta) : Time_1
G |- d : DerivedTime(P) G |- w : Rewrite(P -> P')
----------------------------------------------------- (Reevaluate)
G |- reevaluate(d, w) : DerivedTime(P')Lift lets any frozen historical time feed into legal consequences. Derive combines a historical time with a derivation witness w : DerivationWitness(P), a record of which rule of pack P produces the derivation, to produce a new derived legal time; Section 3.3 defines the witness type and fixes derive_1(t, w) as the abbreviation of derive_1(t, P, w). The pack-evolution witness RewriteWitness is a different object, and only Reevaluate consumes it. For example, an incorporation date (Time_0) combined with a filing rule produces a deadline (Time_1). Toll adds an admitted exclusion to the deadline’s support set. Its input binds the claim, rule, calendar, qualifying interval, and source evidence. Section 7.8 defines its union normalization. Repeated or overlapping support contributes time once. Nesting Toll therefore preserves the original base deadline and all distinct grounds, while recomputing the combined elapsed-time effect.
Reevaluate computes the post-rewrite consequence from a derived-time closure and a typed pack rewrite witness without invalidating the original term.
Time_0 and Time_1 are abstract sorts. Their introduction forms are not constructors for Match-Dep, and no match motive ranges over a temporal scrutinee. The source projection src_0 exists only at the metalevel. No primitive rule therefore eliminates a Time_1 into a Time_0. A constant function of type Pi(x : Time_1). Time_0 remains derivable; proving that its result cannot depend on x is the open noninterference theorem of Section 10.12.
Unindexed temporal proposition sugar. Fix evaluator event time t_e and a pack-declared non-negative bound H. The local horizon is [t_e,t_e+H]. These forms abbreviate the indexed forms on that horizon; they do not add a second temporal calculus.
G |- phi : Prop
------------------- (Eventually-Temporal)
G |- diamond phi : PropG |- phi : Prop
--------------- (Always-Temporal)
G |- box phi : PropThe operators diamond phi and box phi desugar to diamond[t_e,t_e+H] phi and box[t_e,t_e+H] phi. Both retain the declared upper endpoint. A bounded interval alone need not contain finitely many time values. Executable bounded quantification additionally requires the pack to supply an explicit finite collection of evaluation points or calendar cells with the coverage property required by its predicate. The endpoint-indexed forms state finite-horizon admissibility; their complete modal metatheory remains open. They are not a behavioral temporal logic for execution traces. A full until operator and branching or clocked trace properties remain open.
Temporal objects combine with tribunal modals to represent authority-relative divergence. Let P_A^1 = Pack(id_A, v_1, rules_A, empty_repeals, 100), P_B^0 = Pack(id_B0, v_0, rules_B0, empty_repeals, 80), and P_B^1 = Pack(id_B1, v_1, rules_B1, empty_repeals, 120). For an event at t = 110, authority A evaluates under P_A^1 while authority B still evaluates under P_B^0. The resulting verdicts inhabit different tribunal modalities and may differ without contradiction. A witness CanonBridge(A, B, Verdict(e)) is required for transport.
4.6 Tribunal Modals
Lex separates an exact issued act from evidence derived under an institution’s rules. An IssuedAct(T,A,v,r,id) records that T, or a permitted delegate, issued the exact value v of schema A for request r. Its identifier names that act. An opaque admission boundary validates the authenticated record. Ordinary proof construction cannot create this type.
The request binds the canonical value and schema, issuer, actual signer, rule-pack digest, immutable context digest, scope, and delegation path. It also binds the issue anchor, validity interval, caller, intended action, and permitted use. Consumable authority includes a stable use identity. The record uses the versioned canonical payload discipline of PCAuth. A signature establishes the attributable act. It does not, by itself, establish every external fact asserted in the value.
DerivedEvidence(T,A,v) records how the value v was obtained under T’s admitted rules. It retains source acts, rule permits, input references, and a checked derivation receipt. A derived result does not assert that T signed that result.
The modal carrier [T]A contains a value v:A and its DerivedEvidence(T,A,v). It is a runtime evidence type, including when A is a proposition. The logical proposition ||[T]A|| forgets the certificate, but cannot authorize execution. Proof erasure preserves the runtime evidence carrier and its references. This distinguishes logical provability, attributable issuance, and policy-authorized derivation within the programming model.
Tribunal ::= NamedTribunal(id) | AmbientG |- A : Sort T : Tribunal
------------------------------------------------ (Tribunal-Form)
G |- [T]A : Type_iHere i=0 for a Prop interface and otherwise equals its type universe level. The runtime certificate data lives in Type_0. Every modal rule threads its premise rows and the local effects shown below. A bridge type carries a latent row eta, just as a function type carries its call effects. The three-argument bridge notation suppresses this declared row for readability. The checked type retains it. Suppressed annotations otherwise retain the displayed threading convention.
Competence and admitted authority records. Fix an authority theory Sigma_auth containing admitted charter, delegation, and recognition clauses. Write T |-auth A when those clauses recognize T’s competence for interface A. This judgment does not assert that any particular act occurred. An Issued node checks competence under the act’s governing policy at issuance. Current action permission uses the current policy separately. The auxiliary preorder <=_auth compares authority interfaces. It is not a subtyping rule on program values.
charter(T, A) in Sigma_auth
--------------------------- (Auth-Charter)
T |-auth A
T1 |-auth A delegate(T1, T2, A) in Sigma_auth
------------------------------------------------ (Auth-Delegate)
T2 |-auth A
T2 |-auth A recognize(T1, T2, A) in Sigma_auth
------------------------------------------------- (Auth-Recognize)
T1 |-auth AT |-auth A0 A0 <=_auth A
--------------------------- (Auth-Sub)
T |-auth AAdmitted act context. Write Delta for authenticated acts, scoped rule permits, and recognition policies admitted by the authority-record verifier. A RulePermit(T,A,B,code(f),r) authorizes execution of the exact typed program f on the specified inputs and context. It binds the program’s closed environment, permitted effects, and use conditions. An authenticated rule pack or delegated capability can issue a reusable permit. Competence alone cannot issue one. Thus a program can apply an authorized rule repeatedly without obtaining a signature for each computed value.
The current-use check validates scope, expiry, revocation, delegation, rule and context digests, and any use limit at the protected action’s admission point. It checks the current authority-state version together with recording that admission. A conflicting authority-state change requires reevaluation. Resumption repeats the current-use check. Historical signature validity remains a separate property of the recorded act. The status function in Section 4.9 supplies the same revocation result to historical classification and current-use policy.
Evidence certificate construction. Certificates are finite directed acyclic graphs with four node forms:
Issued(a)refers to one admitted exact-value issued act.Computed(d,f,inputs,v,trace)records an admitted rule permit, exact program, typed inputs, output, context, and execution receipt. Its sources include the rule permit and all evidence dependencies.Recognized(b,m,decision)retains the source certificate and adds the checked destination evidence-acceptance decision.Cut(m,n)joins an opened evidence dependency to the continuation’s result certificate. It creates no issued act.
The certificate checker verifies exact value and context bindings at every node. It recomputes pure steps and checks recorded primitive transitions against their admitted evidence. It never replays an external action while checking its receipt. Computed nodes retain all source acts. Recognized nodes retain the original issuer and recognition path. Cut nodes retain the union of their dependencies. Node sharing reuses evidence without representing another issuance.
Modal rules. The following rules write their authority context explicitly. A checked rule or recognition permit remains subject to the current-use check when its protected operation executes.
a : IssuedAct(T,A,v,r,id) in Delta T |-auth A
------------------------------------------------- (Tribunal-Assert)
G; Delta |- assert[T](a) : [T]A [empty]G; Delta |- m : [T]A [rho_m]
G; Delta |- f : Pi(x:A)[rho_call].B [rho_f]
d : RulePermit(T,A,B,code(f),r) in Delta
------------------------------------------------- (Tribunal-Derive)
G; Delta |- derive[T,d](f,m) : [T]B
[rho_m union rho_f union rho_call
union {authority(T)}]G; Delta |- m : [T1]A [rho_m]
G; Delta |- b : CanonBridge(T1,T2,A;eta_b) [rho_b]
------------------------------------------------- (Tribunal-Coerce)
G; Delta |- coerce[b](m) : [T2]A
[rho_m union rho_b union eta_b]G; Delta |- m : [T]A [rho_m] T |-auth (A -> B)
G,x:A,p:EvidenceRef(T,A,x); Delta |- e : [T]B [rho_e]
------------------------------------------------- (Tribunal-Open)
G; Delta |- open_T m as (x,p).e : [T]B [rho_m union rho_e]G; Delta |- e : [T]B [rho_e]
G; Delta |- b : CanonBridge(T,Ambient,B;eta_b) [rho_b]
------------------------------------------------- (Tribunal-Adopt)
G; Delta |- adopt[b](e) : B [rho_e union rho_b union eta_b]Tribunal-Assert imports an already issued act into its evidence carrier. It is pure and issues no new act. Tribunal-Derive executes the permitted program and constructs a Computed certificate. The displayed form has a fixed result interface. The dependent form uses B[v/x] for the input value v; its receipt binds that input and result schema. Functions retain their latent effect rows under both forms. Higher-order programs therefore use the ordinary Pi and application rules instead of a special manual approval path.
Tribunal-Coerce checks the receiving policy before creating Recognized evidence. That value means acceptance under the destination policy, not a fresh assertion signed by the destination. A separate local-action check still preserves the destination’s reserved decisions. An unavailable bridge decision suspends or rejects that recognition use without deleting the source evidence.
Tribunal-Open supplies the value and an opaque, value-indexed reference to its provenance. The continuation can apply an admitted rule to that evidence and return a derived result. It can also return independently issued evidence. The Cut certificate records the opened dependency in either case. The continuation needs no fresh signature merely because its computed value differs from the input.
Tribunal-Adopt checks explicit recognition into the evaluator’s ambient authority. It returns the value and retains the adoption receipt in the execution evidence. The bare value is neither an issued act nor an authority capability. A later institutional action still checks its own exact request and authority requirements.
Issuing a new act. A new issuance is a separate operation under a checked IssueCap. It binds the exact value before issuance and produces a new admitted act record. Its declared effects include authority(T), attest(T), and the relevant write scope. The result includes its act identifier. Op and the authority-record verifier mediate the protected mutation. A permitted institutional program can perform this operation autonomously. Derivation and receipt checking do not call it.
The runtime transitions construct certificates explicitly:
assert[T](a) --> evidence(value(a), Issued(a))
derive[T,d](f, evidence(v,p))
--> run_rule(d,f,v,p)
-- run_rule checks current use, evaluates f v, and returns
-- evidence(w, Computed(d,f,[p],w,trace)).
open_T evidence(v,p) as (x,q).e
--> join_evidence(p, e[v/x,p/q])
-- join_evidence(p,evidence(w,n)) --> evidence(w,Cut(p,n)).
coerce[b](evidence(v,p)) --> run_bridge(b,evidence(v,p))
-- Identity returns the same carrier.
-- A primitive step checks acceptance and adds Recognized.
-- Composition runs its primitive steps in order.These internal constructors are created by checked transitions. Source programs cannot forge EvidenceRef, an issued act, or a certificate by supplying unchecked fields. Substitution retains value indices, latent bridge rows, and provenance references. A request or context change requires the corresponding rule-use and evidence checks again.
Proposition (issued-act provenance and derived evidence). Every issued-act reference in a well-typed runtime result originates in an admitted input act or a permitted issuance transition. Assert, derive, open, coerce, and adopt cannot invent an issued-act reference. Every derived certificate identifies its rule permit, exact input bindings, and retained source acts.
Proof construction. Induct on the actual runtime transition. Assert uses its admitted input. Derive adds a Computed node whose children are the validated rule permit and input certificates. Primitive results enter only through their typed admission contracts. Open adds Cut after value-indexed substitution. Coerce adds Recognized and preserves its source. Adopt records the same certificate under its checked destination decision. The issuance rule is the only case that adds a new issued act, and its premise checks the issuance capability. The certificate checker independently verifies each node’s binding and children. Induction gives provenance preservation for every finite execution prefix, including suspension and reuse. Its mechanization requires proofs of signature validation, capability admission, typed substitution, and compiler preservation.
Bridges act covariantly on admitted evidence carriers. Their operational meaning includes destination acceptance and retained provenance. A bridge action does not order tribunals or combine their local authority into a universal permission. Distinct bridge paths can produce equal payloads while retaining different provenance certificates.
Bridge witnesses are generated from admitted bilateral recognition evidence. A bridge names its rule record and scope. Every protected use checks destination evidence acceptance at the applicable view. The static bridge type does not grant a destination action permission. A primitive receiving rule declares all its effects, including its local authority checks. Identity has latent row empty. Composition unions the latent rows of its two component bridges. Thus intermediate jurisdictions remain visible in the effect budget.
T |-auth A
------------------------------- (Bridge-Id)
G |- id_T^A : CanonBridge(T, T, A; empty)T1 |-auth A T2 |-auth A
r : mutual_recognize(T1,T2,A;eta_r) in Sigma_auth
------------------------------------------------------ (Bridge-Mutual)
G |- bridge[r,T1 => T2,A] : CanonBridge(T1,T2,A;eta_r)G |- b12 : CanonBridge(T1,T2,A;eta12)
G |- b23 : CanonBridge(T2,T3,A;eta23)
------------------------------------------------------ (Bridge-Comp)
G |- b23 * b12 : CanonBridge(T1,T3,A;eta12 union eta23)Operational bridge interpretation. A bridge program is an identity, a primitive receiving rule, or an ordered composition. Its interpreter takes a runtime state and an evidence carrier. It returns a completed result, rejection, or a suspended continuation, together with the resulting state and event trace.
run_bridge(id, S, m) = Done(S,m,[])
run_bridge(primitive(r), S, evidence(v,p)) =
check_receive(r,S,v,p)
-- On acceptance: Done(S',evidence(v,Recognized(r,p,decision)),events).
-- On rejection or suspension: retain that outcome and its evidence.
run_bridge(b23 * b12, S, m) =
bind(run_bridge(b12,S,m),
(S1,m1) => run_bridge(b23,S1,m1))Here bind concatenates event traces in order. It propagates rejection and retains a suspended continuation with the completed prefix’s certificates. Identity performs no receiving check and adds no certificate node. A protected action reached after identity transport still undergoes its separate action-admission check. Composition visits every primitive rule in order and retains every acceptance decision.
Define operational bridge equality by equality of these interpreter outcomes for every well-typed input and admissible primitive-response sequence. Equality includes state changes, event traces, value indices, source acts, and provenance certificates. Certificate normalization permits structural identity, association, and shared-node references. It preserves primitive decisions, scopes, timestamps, original act identities, and the order of dependency checks. Payload equality alone does not establish operational bridge equality.
Proposition (operational bridge laws). Identity interpretation is a left and right identity. Composition is associative. Operational equality is an equivalence relation and is preserved by composition.
Proof construction. Identity returns the unchanged state and carrier with an empty trace. Binding that result changes no later transition. Both parenthesizations of three composed bridges visit the same primitive rules in order. They retain the same intermediate states, traces, decisions, and suspended continuation. Structural association only changes the representation of that ordered program. Pointwise reflexivity, symmetry, and transitivity establish equivalence. Replacing a component by an equal interpreter preserves the input to the next component and all accumulated evidence. \square
Existing function-bridge result. BridgeSemantics.v proves the corresponding identity, composition, congruence, and strict function-bridge laws for an abstract total-function target. In particular, it carries function_bridge_strict_2functor_coherence. That target can describe a payload interpretation after the relevant acceptance conditions are fixed. It does not itself represent rejection, suspension, stateful current-use checks, or certificate identity.
The runtime adequacy proof must connect the actual bridge syntax to the interpreter above, prove its latent-row effect bound, and establish its operational laws with certificate preservation. An additional projection lemma can relate completed runtime outcomes to the existing function target. That projection cannot identify runtime certificates solely because their payloads agree.
Competence checking has a finite search interpretation. Begin with admitted charters, then add each judgment justified by a delegation or recognition rule. The next theorem establishes termination under its finite-interface and decidable-order premises.
Theorem (finite authority recognition is decidable). Assume Sigma_auth contains finitely many charter, delegation, recognition, and mutual-recognition clauses. Let I be the finite set of interfaces named in Sigma_auth or in the query, and let T be the corresponding finite set of tribunals. Assume <=_auth is decidable on I. Then derivability of the query T_q |-auth A_q is decidable.
Proof. Put V := T × I. Consecutive Auth-Sub steps compose by transitivity of <=_auth. Every derivation therefore normalizes so that its intermediate judgments use interfaces named in a clause or in the query. Define F : P(V) -> P(V) to add exactly the pairs justified by one authority rule whose premises are already present. Iteration from the empty set reaches the least fixed point because V is finite. Each round is decidable. Soundness follows from the definition of F; completeness follows by induction on normalized derivations. Membership of (T_q, A_q) in the fixed point decides the query. \square
This procedure decides competence from a fixed, finite authority theory. Act admission and current-use checks require their own evidence. Tribunal modal terms themselves remain outside the admissible term fragment of Section 5 until the stratification conditions for modal reduction are proved.
Hypothetical ADGM/DIFC mutual-recognition example. The receiving institutions are the Dubai International Financial Centre (DIFC) and its Dubai Financial Services Authority (DFSA). Assume the recognition instrument specified below for this example. To show the rule, let A := FitAndProper(d) and assume a future bilateral instrument adds:
charter(ADGM_FSRA, A), charter(DIFC_DFSA, A), recognize(ADGM_FSRA, DIFC_DFSA, A), recognize(DIFC_DFSA, ADGM_FSRA, A), mutual_recognize(ADGM_FSRA, DIFC_DFSA, A).
Then:
charter(ADGM_FSRA, A) in Sigma_auth
----------------------------------- (Auth-Charter)
ADGM_FSRA |-auth A
charter(DIFC_DFSA, A) in Sigma_auth
----------------------------------- (Auth-Charter)
DIFC_DFSA |-auth ARecognition also gives explicit cross-side derivations:
DIFC_DFSA |-auth A recognize(ADGM_FSRA, DIFC_DFSA, A) in Sigma_auth
----------------------------------------------------------- (Auth-Recognize)
ADGM_FSRA |-auth A
ADGM_FSRA |-auth A recognize(DIFC_DFSA, ADGM_FSRA, A) in Sigma_auth
----------------------------------------------------------- (Auth-Recognize)
DIFC_DFSA |-auth AFrom bilateral derivability and the mutual-recognition clause we obtain the concrete bridge
b_AD : CanonBridge(ADGM_FSRA, DIFC_DFSA, A)
by Bridge-Mutual, and symmetrically b_DA. Supply an independently admitted act:
a_AD : IssuedAct(ADGM_FSRA,A,p,r_AD,id_AD) in Delta
adgm_evidence := assert[ADGM_FSRA](a_AD)
recognized_evidence := coerce[b_AD](adgm_evidence)The first carrier contains the exact value p and its Issued certificate. The second retains id_AD and adds the destination recognition decision. Bilateral competence supplies the bridge context. The admitted act establishes that this particular issuance occurred.
An admitted DIFC rule can then derive its local verdict automatically:
verdictOf : A -> ComplianceVerdict
d_D : RulePermit(DIFC_DFSA,A,ComplianceVerdict,
code(verdictOf),r_D) in Delta
local_verdict := derive[DIFC_DFSA,d_D](verdictOf,recognized_evidence)The rule-use check binds the exact value, context, and permitted effects. The result has type [DIFC_DFSA]ComplianceVerdict and retains the original ADGM act, recognition decision, and DIFC rule receipt. It does not claim that DIFC signed the computed verdict. Explicit ambient adoption is required to obtain a bare ambient verdict:
opened : [DIFC_DFSA]ComplianceVerdict :=
open_DIFC_DFSA recognized_evidence as (x,p).
derive[DIFC_DFSA,d_D](verdictOf,recognized_evidence)
b_DA : CanonBridge(DIFC_DFSA,Ambient,ComplianceVerdict;eta_DA)
ambient_verdict : ComplianceVerdict := adopt[b_DA](opened)Here verdictOf : Pi(x:A)[empty].ComplianceVerdict is a supplied pure rule, and DIFC_DFSA |-auth (A -> ComplianceVerdict) is part of its competence context. Tribunal-Derive produces the modal result required by Tribunal-Open. The open step adds its Cut dependency. Tribunal-Adopt consumes the explicit bridge. Its effect row joins derivation’s authority effect with eta_DA. Replacing the open body by the bare expression verdictOf x fails its modal-result premise. A new institutional action separately checks its local authority requirements.
The surface syntax requires the witness explicitly: coerce[T1 => T2](e, w). A surface form that elides the witness is not accepted by the elaborator; no default or placeholder witness is supplied, because a coercion without a named bridge witness is the exact failure mode the tribunal modal is designed to prevent.
4.7 Typed Discretion Holes
The governing rule pack declares a hole signature sig_P: a finite map assigning each hole identifier h its value type tau_h together with either the responsible authority and declared scope (discretion holes) or the unsettled domain (unsettled holes). A well-formed signature excludes the empty value type 0, CanonBridge(T1,T2,A), and tribunal-modal types [T]A. These types require their own authority constructors and cannot be supplied by one officer’s PCAuth witness. The hole rules draw their premises from that signature, so a hole term types only at its signature-declared type.
G |- e : A [empty]
----------------------------------------------- (MechanicalHole)
G |- MechanicalHole(h, e) : A [empty]
sig_P(h) = DiscretionSig(auth, tau_h, S) G |- tau_h : Type_i [empty]
----------------------------------------------------------- (DiscretionHole)
G |- DiscretionHole(auth, h, S) : tau_h [discretion(auth)]
sig_P(h) = UnsettledSig(dom, tau_h) G |- tau_h : Type_i [empty]
------------------------------------------------------------ (UnsettledHole)
G |- UnsettledHole(dom, h) : tau_h [unsettled(dom)]MechanicalHole marks a site whose answer is already within the core of settled meaning. It carries the empty effect row and reduces immediately to its mechanically derived witness e. DiscretionHole marks Hart’s penumbra: the term is well typed, but it emits discretion(auth) and cannot reduce further until an authorized human supplies a fill. UnsettledHole emits unsettled(dom), a different effect: no existing authority may discharge it with a PCAuth witness, because the present rule pack has no disposition to apply. Both hole forms are well typed in the full calculus and both are rejected by the admissible fragment (Section 5), for different reasons: one requires an authorized judgment; the other requires lawmaking.
Discretionary filling uses the admitted request and its exact answer:
sig_P(h) = DiscretionSig(auth, tau_h, S)
G |- e : tau_h [empty] G |- w : PCAuth(auth, h, e, request(h,e)) [empty]
--------------------------------------------------------------------- (Fill)
G |- fill(h, e, w) : tau_h [empty]
G |- e : tau_h [empty] G |- w : PCAuth(auth, h, e, request(h,e)) [empty]
--------------------------------------------------------------- (RecordFill)
G |- RecordedFill(h, e, w) : FilledDiscretionHole(h)G |- fills : List(FilledDiscretionHole(h))
----------------------------------------- (Precedent)
G |- Precedent(h, fills) : PrecedentChain(h)G |- f : FilledDiscretionHole(h)
G |- e' : tau_h G |- w' : PCAuth(higher_auth, h, e', request(h,e'))
------------------------------------------------------------------- (Appeal)
G |- Appeal(f, higher_auth, e', w') : AppealedFill(h, f, higher_auth)
G |- r : PackRewrite(dom, P, P') G[P'] |- e : tau_h [empty]
-------------------------------------------------------------- (PackRewrite)
G[P] |- settle(h, r, e) : tau_h [empty]Fill discharges the hole: the filling e must have the hole’s signature type tau_h, and the witness w must prove that the filler has authority auth for the exact judgment (h, e) and the exact request, pack, and context digests; changing the value or the context changes the witness type. The filled result is pure: the discretion effect is discharged, so downstream computation proceeds without further human input. RecordedFill materializes the audit object that later precedent chains and appeals consume. Precedent packages a typed chain of past fills for consultative use; later fillers may cite it but are not bound by it. Appeal records a higher-authority re-fill, and downstream verdicts depending on f are tagged Appealed until re-derived. PackRewrite is the only eliminator for UnsettledHole: it requires a typed witness that the governing rule pack has evolved from P to P’ and re-runs the derivation under P’. No individual PCAuth witness can discharge unsettled(dom).
For holes whose policy requires a quorum, the witness type is refined to PCAuth_k(auth, h, e, request(h,e)), meaning that the same value-indexed witness additionally certifies a k-of-n threshold over the exact value e and request context.
Revocation is typed rather than ambient. We use Depends(j, c) for the transitive dependency judgment on derivation traces: it holds when credential c occurs anywhere in the justification tree of judgment j. We also write Tagged(A, s) for a value of type A tagged with status s in {Honored, Tainted, Invalid}.
A CompleteStatusInput contains the complete credential chains, authenticated revocation coverage through a declared horizon, and the required anchor comparisons. Section 4.9 specifies this input. An individual revocation produces credential-timing evidence. It does not independently set the status of the whole verdict.
G |- r : RevokedCred admit_revocation(B,r) = Accepted
------------------------------------------------------ (Admit-Revoke)
G |- r : AdmittedRevocation(subject(r),B)G |- w : AuthorityWitness G |- r : AdmittedRevocation(c,B)
c in chains(w) anchor(w) < position(r)
------------------------------------------------------ (Credential-Later)
G |- later_evidence(w,c,r) : CredentialTiming(w,c,B,Later)G |- w : AuthorityWitness G |- r : AdmittedRevocation(c,B)
c in chains(w) position(r) <= anchor(w)
------------------------------------------------------ (Credential-Invalid)
G |- invalid_evidence(w,c,r) : CredentialTiming(w,c,B,Invalid)G |- j : A B : CompleteStatusInput(j,H)
s = max_{w in authority_sources(j)} tag_B(w)
------------------------------------------------------ (Verdict-Status)
G |- classify(j,B) : Tagged(A,s)Here AuthorityWitness denotes an anchored authority record in the complete provenance graph. It includes PCAuth fills, issued acts, and the authority records supporting rule and recognition permits. Each record supplies its own anchor and complete credential chains. tag_B(w) is the exclusive function of Section 4.9. Verdict-Status takes the maximum across all records in the graph. For a complete graph with no authority sources, this revocation axis has value Honored. That value grants no new authority.
Credential-Later and Credential-Invalid classify one credential relative to its source anchor. They cannot construct Tagged(A,Tainted) or Tagged(A,Invalid) directly. The unique aggregate rule supplies those whole-verdict tags. A complete verdict input supplies the per-source projection used by tag_B(w) for each source w. Signed wall-clock fields remain assertions. Comparable authenticated bulletin positions determine the order. A missing chain member, coverage range, or required comparison leaves classification pending.
Delegation is explicit and depth-bounded. A root authority credential AuthorityCred(auth, p, S) says that principal p holds authority auth over scope S. DelegateCred(auth, p, q, S, d) says that principal p delegates that authority to principal q over sub-scope S with residual depth d.
G |- c : AuthorityCred(auth, p, S) G |- q : Did G |- S' subseteq S d >= 0
------------------------------------------------------------ (Delegate-Root)
G |- delegate(c, q, S', d) : DelegateCred(auth, p, q, S', d)
G |- delta : DelegateCred(auth, p, q, S, d+1) G |- r : Did G |- S' subseteq S
------------------------------------------------------------ (Delegate-Step)
G |- delegate(delta, r, S', d) : DelegateCred(auth, q, r, S', d)Lemma (delegation does not expand authority). If delta : DelegateCred(auth, p, q, S’, d) is derivable from a root credential over scope S, then S’ subseteq S and every delegation chain ending in delta has length at most the root depth bound. Hence a delegated signer can exercise only authority already present at the root and cannot increase delegation depth.
Proof sketch. By induction on the delegation derivation. Delegate-Root imposes the scope inclusion S’ subseteq S directly. Delegate-Step preserves inclusion by premise and strictly decreases residual depth from d+1 to d. Transitivity of subset across the chain yields the scope claim, and the strictly decreasing depth yields the bound.
G |- e : A [empty] G |- W : PCAuth_k(auth, h, e, request(h,e)) [empty]
G |- fresh(id(h)) G |- required(h) = k
G |- W.signers subseteq committee(h) G |- |committee(h)| <= n_max
-------------------------------------------------------------- (Fill-Quorum)
G |- fill_k(h, e, W) : A [empty]Fill-Quorum is the multi-signer form. At hole introduction, a committee-policy DiscretionHole carries two pieces of pack-data: a declared committee committee(h) : Finset(Did) (the finite set of principals whose joint determination is legally required) and a threshold required(h) : Nat. The default is a singleton committee with required(h) = 1; committee holes specify both at introduction. A witness W : PCAuth_k(auth, h, e, request(h,e)) is well-formed only when W.signers subseteq committee(h), |W.signers| >= k, and k = required(h). The value index e is shared: every signer commits to the same verdict and the same fill-request, pack, and proof-context digests. Duplicate signer counting is ruled out by DistinctSigners(signers) combined with the subset constraint; replay into a different hole or request is ruled out by the signed canonical payload. The deployment bound n_max of the forgery reduction is the type-level upper bound on |committee(h)| under the deployed authority pack, not a reduction-side slack parameter; the reduction simply exposes it as the slot-guessing denominator.
4.8 Delegation Chains
A single authority rarely signs every discretionary decision itself. A regulator delegates signing authority to specific officers; those officers may further delegate to named deputies within documented scope limits. Lex makes this chain typed and bounded.
Section 4.7 measures the delegation depth remaining. Here d counts signed links already traversed, so Chain-Step increases it. This path supplies the evidence inspected at fill time.
-- Delegation types
Delegate(a : Authority, s : Authority, scope : Scope) : DelegationEdge
DelegationChain(root : Authority, leaf : Authority, d : Nat) : Type
AuthorityChain(root, leaf, d) := DelegationChain(root, leaf, d) (Chain-Base)
G |- refl(auth) : DelegationChain(auth, auth, 0)
G |- c : DelegationChain(auth, s, d)
G |- e : Delegate(s, s', sigma) d + 1 <= d_max
--------------------------------------------------- (Chain-Step)
G |- ext(c, e) : DelegationChain(auth, s', d+1)Chain-Base and Chain-Step introduce and extend a delegation chain. A root authority has a reflexive chain to itself of depth 0. A chain of depth d from root auth to intermediary s extends to a chain of depth d+1 to s’ given a signed delegation edge s -> s’ scoped by sigma, provided the new depth does not exceed the bound declared by the pack; the examples use 4. A chain exceeding that bound is not well typed.
A delegation edge Delegate(a, s, scope) is itself an attested record:
Delegate(a, s, scope) = {
issuer : Did, -- a's signing principal
delegate : Did, -- s's principal
scope : Scope, -- restriction on what s may sign under a
issued_at : Time_0,
stamp : BulletinStamp,
signature : Ed25519Sig(issuer,
bind_del(a, s, scope, issued_at))
}The chain’s chain_digest is the Merkle root of the ordered edge signatures. The effective scope is sigma_0 cap ... cap sigma_d. Delegation-edge issuance proves that each child scope is contained in its parent. At fill time, scope_ok proves that the signed value belongs to both this effective scope and the hole scope.
Delegation chains compose: refl is the empty chain, ext appends one signed edge and increments depth, and chains beyond d_max are ill-typed under the deployed pack. The effective scope of a chain is the meet of its edge scopes in the semilattice of §3.5, so scope only shrinks along a chain. Revocation and pack-rewrite never reverse a chain: they act through the bulletin (§4.9, §4.10) and tag downstream verdicts Tainted or Invalid.
Proposition (Delegation soundness). If G |- w : PCAuth(auth, h, v, r) is well typed and one authority chain has depth d <= d_max, then there exists a sequence p_0,...,p_d with p_0 = auth and p_d the signer. Each link is signed by its predecessor, each edge scope is contained in the preceding scope, and v belongs to the intersection of the effective chain scope and h.scope. Structural induction on the chain proves the statement.
4.9 Revocation and Temporal Tagging
Credentials outlive any single judgment. An officer who holds an authorized-signer credential at t_1 may have that credential revoked at t_2 > t_1 for cause. Verdicts derived from a filling at t_1 remain in the audit record; the question is how to characterize their status once the revocation is recorded. Lex fixes this characterization by types.
-- Revocation artifact
Revoke(c : Credential) : RevokedCred =
{ target : Credential,
reason : RevocationReason,
revoked_at: Time_0,
stamp : BulletinStamp(t_r),
signature : Ed25519Sig(issuer_of(c),
bind_rev(c.id, t_r, reason))
}
-- Status tag on a derived verdict
VerdictStatus ::= Honored | Tainted | InvalidFor each credential c in each authority chain of w, compare anchor(w) with the earliest authoritative revocation of c through the complete input’s declared horizon. The witness tag is the maximum of all credential tags in the order Honored < Tainted < Invalid. Thus every credential in every chain participates in the result. For a derived verdict, Section 4.7 then takes the maximum across its complete authority-source graph, using each source’s own anchor.
Complete status evidence. The admitted input B:CompleteStatusInput(w,H) binds the exact witness, all used credential chains, the governing authority policy, and a declared horizon H. The horizon must cover the witness anchor. Each chain must reach its declared trust anchor through authenticated parent links. The input includes complete applicable revocation coverage for every chain credential through H.
Coverage can use a complete authenticated bulletin prefix or an equivalent issuer-scoped query proof. The proof must establish the applicable revocation set through the horizon, including authoritative absence when that set is empty. Every required range and issuer must be covered. A positive inclusion path proves one entry, not completeness or absence. Earliest-revocation selection requires the same complete coverage, including when a later revocation is already visible.
A revocation after the source anchor supports Tainted only when complete coverage excludes an earlier revocation. An earlier revocation would instead require Invalid.
The input also authenticates each source anchor and supplies a comparable position for every relevant revocation. Distinct bulletins require the admitted comparison witness of Section 4.10. A derived verdict combines these inputs for every authority source in its complete provenance graph. The completeness claim is relative to the declared authoritative channels and publication policy. That institutional publication obligation remains part of the deployment assumptions.
Evidence preparation returns either a complete input or PendingEvidence. Missing ranges, chains, issuer coverage, or comparison evidence cannot become an empty revocation set. The status function below accepts only the complete input.
-- B : CompleteStatusInput(w,H)
-- first_B(c) is the earliest authoritative Revoke(c) through H.
-- None means an authoritatively empty set proved by B.
invalid_B(w) :=
exists c in chains(w),
first_B(c) = Some rv and rv.stamp.position <= anchor(w)later_B(w) :=
exists c in chains(w),
first_B(c) = Some rv and anchor(w) < rv.stamp.positiontag_B(w) :=
if invalid_B(w) then Invalid
else if later_B(w) then Tainted
else HonoredG |- w : AuthorityWitness B : CompleteStatusInput(w,H)
not invalid_B(w) not later_B(w)
------------------------------------------- (Status-Honored)
G |- tag_B(w) = HonoredG |- w : AuthorityWitness B : CompleteStatusInput(w,H)
not invalid_B(w) later_B(w)
------------------------------------------- (Status-Tainted)
G |- tag_B(w) = TaintedG |- w : AuthorityWitness B : CompleteStatusInput(w,H)
invalid_B(w)
------------------------------------------- (Status-Invalid)
G |- tag_B(w) = InvalidThese rules partition witnesses relative to the identified bulletin snapshot. Status-Invalid takes precedence whenever any chain credential was revoked at or before the witness anchor. Status-Tainted requires a later revocation and the absence of any such invalidity. Status-Honored requires neither condition. Each result records the complete-input digest, declared horizon, comparison witnesses, and decisive revocation evidence. Incomplete coverage leaves the check pending, even when some entries are visible. It does not produce Honored.
The tag describes the historical witness relative to admitted evidence. A new institutional action separately checks current authority, expiry, scope, delegation, rule version, and the exact intended use. The same status function supplies the revocation input to that check. A later use can therefore fail while the original act remains in the historical evidence record.
-- Retain historical evidence with its derived status.
status_record := classify_with_evidence(B, verdict)
record_status(verdict, status_record)
-- New actions additionally check current authority and intended use.
admit_use(verdict, action, current_view) :=
current_use_check(verdict, action, current_view, status_record)When a source anchor and its revocation stamp share a bulletin, their log positions supply the comparison. Across bulletins, the complete input carries an admitted comparison witness. Classification remains pending when that comparison cannot be established. The bulletin does not prove real-world event time by itself; it proves that, once an entry is anchored under the publication policy, the operator cannot later change its Merkle position without detection. The temporal comparison is visible in the derivation trace and reproducible from the bulletin plus the deployment’s submission policy.
Proposition (Revocation determinism). For every well-typed authority witness w and complete finite status input B, exactly one status rule applies. Taking the maximum over a complete finite provenance graph likewise gives one verdict status.
Proof. If invalid_B(w) holds, only Status-Invalid applies. Otherwise, later_B(w) selects exactly one of Status-Tainted and Status-Honored. Complete coverage establishes the finite applicable revocation set. The earliest revocation exists uniquely whenever that set is nonempty. The admitted comparison relation supplies the required total order. The resulting function equals the maximum of all credential tags in the stated severity order. For a fixed witness, dependency graph, authority policy, and comparison relation, extending complete coverage to a later horizon can preserve or increase that maximum. It cannot decrease it. \square
The full verdict-status lattice is the product poset {Honored, Tainted, Invalid} x {Live, Appealed} with coordinatewise order Honored < Tainted < Invalid and Live < Appealed. The trichotomy above is the projection onto the revocation axis; it is deterministic under the complete-input and comparison requirements above. Appeal (§3.5, §4.7) is orthogonal: a verdict can be (Tainted, Appealed) (the witness’s credential was later revoked and a higher authority issued a re-fill) or (Honored, Appealed) (the witness remains honored and a higher authority nonetheless re-filled) without either coordinate collapsing the other. The section’s Status-Honored/Tainted/Invalid rules and §3.5’s Appeal rule therefore fire on disjoint axes and compose by product. The richer lifecycle coordinates discussed in §12.9 (speech-act force, acknowledgment, affirmance) would extend this lattice with a third factor; the present paper fixes only the two orthogonal factors already supported by the calculus.
Bitemporal assessment and current use. An assertion can be recorded after the time to which it refers. Legal effect can also begin before its notice becomes visible. These axes belong to each assessment, rather than to a single timestamp interpreted differently by each host.
An evidence event retains its stable assertion and occurrence identities. It records an asserted occurrence time, signature time, independently admitted anchor, observation position, and legal effective interval when applicable. A signature authenticates its payload. Its claimed signing time is distinct from the independently established anchor. An observation position orders knowledge in one authenticated history. Cross-history comparison requires the admitted evidence of Section 4.10. Legal dates use their named jurisdictional calendar.
The shared query context is \tau=(t_{\rm legal},K,t_{\rm decision},t_{\rm use},\sigma), Here t_{\rm legal} is the legal time being assessed, t_{\rm decision} is the decision time, and t_{\rm use} is the intended action time. The value K identifies the admitted evidence view and \sigma names the authority-use stage. That stage can be judgment, commitment, dispatch, provider acceptance, or external effect. The governing institution specifies which stage requires current authority.
SupportedThen(request,decision_id,K_then)
LegalAssessment(request,t_legal,K,policy)
UsePermit(request,revision,stage,t_use,K,current_policy)SupportedThen reconstructs the evidence and rules actually used for a recorded decision. LegalAssessment determines the legal consequence at the queried legal time under the selected evidence view and policy. Its result can be valid, invalid, disputed, or pending. UsePermit authorizes a particular current action at its stated stage. None of these types coerces to another. A later view can change the assessment of an earlier event while preserving the earlier SupportedThen record.
The revocation function above classifies credential evidence relative to its source anchors and complete bulletin view. That status is an input to legal assessment, rather than a universal legal-validity decision. An ordinary revocation carries its effective scope and time. A later compromise notice can identify an earlier compromise interval. A stay can prohibit further execution while leaving an earlier signature record intact. Each legal consequence requires its governing rule, competent authority, and exact subject. Conflicting authoritative accounts remain disputed until the governing procedure resolves them. A technical administrator’s changed configuration supplies no such act.
Select evidence by observation position K, then select its legal applicability at t_{\rm legal}. Resolve supersession only through an admitted, acyclic authority relation. Preserve all predecessor records. An unrelated later timestamp is insufficient to supersede an act. A constitution or rule-pack amendment follows its own authorized transition, including adoption, commencement, appeal, and succession conditions. It cannot rewrite the authority root that permitted it.
Proposition (historical reproducibility). Fix a history prefix, request, policy, and deterministic evaluator. Appending new observations leaves its SupportedThen result unchanged. A legal assessment at a later evidence view may differ, including for the same legal time.
Proof. Prefix selection yields the identical input sequence after append. The request and policy are also identical, so induction over the evaluator’s deterministic steps yields the same derivation. A later view includes further premises. The evaluator then has a different input and can produce a distinct assessed consequence. Both derivations remain indexed by their own views. \square
For example, an admitted grant supports a permitted instruction. A compromise notice observed later can place that instruction’s present assessment in dispute from an earlier effective date. Its historical record and actual provider occurrence remain. A later authorized resolution can restore current eligibility through a new assessment. An ordinary prospective revocation instead blocks its scoped future uses without changing the recorded signature check at the old view.
Continuation and replay. A suspended continuation retains the immutable pending record, request revision, program, pack, authority context, dependencies, reservations, and outstanding obligations. A response must answer that exact authenticated question. Resolution records its historical answer under the original conditions. Continuing the workflow separately checks current authority at the required stage. An expired capability therefore does not erase the answer or authorize a new use. An authorized successor request can carry unanswered obligations and existing resource reservations through an explicit transition. Supersession itself supplies no answer.
Replay has type History -> ReconstructedState and an empty dispatch-capability context. It consumes recorded provider occurrences, not provider adapters. The dispatcher has a separate capability and resumes commands by their stable pre-dispatch identifiers. A new compensating transfer receives its own command and occurrence.
Theorem (replay separation). Replaying a finite admitted history preserves its command and occurrence identifiers and emits no external dispatch. Applying a later correction can change an assessment without reissuing any recorded payment.
Proof. Every replay clause reads one event and updates an internal projection. No clause possesses a dispatch capability or calls an adapter. Induction on the history gives an empty dispatch trace. Provider-event clauses copy their recorded identities. Correction clauses append assessment links and preserve those events. The dispatcher is a distinct transition requiring a command record and current-use premises. \square
With unchanged authority, an answered continuation can resume and complete automatically. After an authorized stay is lifted, fresh current-use evidence can permit the retained command to proceed under its original identity. Historical reconstruction never performs that execution. These types are the Lex contract for Op, the Sovereign Jurisdiction Network, and Recourse. Their adapters must preserve the indices and separate replay from dispatch.
4.10 Bulletin-Anchored Timestamps
The public bulletin that anchors BulletinStamp is the Haber-Stornetta (1991) append-only Merkle log: every anchored entry is a leaf of a growing Merkle tree whose roots are periodically published (canonical implementation: certificate transparency logs or an equivalent public bulletin service). A BulletinStamp(t) consists of: (a) the leaf index t (an integer position in the append-only log, serving as the public time coordinate), (b) a Merkle inclusion proof from the leaf to a published root, and (c) a signed root attestation from the bulletin operator.
BulletinStamp(t) = {
position : Nat, -- Merkle-log leaf index
inclusion : MerklePath, -- path from leaf to root
root_sig : Ed25519Sig(bulletin_operator, root_at_epoch(t))
}A witness’s stamp binds the witness into a total order over the log’s leaves. Two witnesses on the same bulletin have comparable timestamps; witnesses on distinct bulletins require a declared BulletinInterop witness specifying how to compare. The security of the Haber-Stornetta construction reduces to collision-resistance of the underlying hash and to append-only integrity of the operator. Inclusion proves membership of a particular leaf. A consistency proof links committed log states. Neither proves that a selected response includes every applicable revocation through a horizon.
Non-revocation and earliest-revocation queries therefore require the complete-prefix or issuer-scoped coverage evidence specified in Section 4.9. The verifier checks the requested horizon, issuer range, and chain identities. It distinguishes a proved empty set from a missing response. The publication policy identifies the authoritative channels whose complete coverage is required.
4.11 Subtyping and Type Inference
Lex has no subtyping relation. Effect weakening enlarges the permitted row while retaining the value type. The authority preorder compares competence interfaces and supplies no coercion between program values. Two types are either definitionally equal under the pure source conversion \equiv_c of Section 4.2, including its stated beta, zeta, annotation, and constrained constructor cases, or they are distinct. A ComplianceVerdict is not a subtype of Nat merely because both support constructor case analysis; a SanctionsResult is not a subtype of ComplianceVerdict despite the semantic proximity of Clear to Compliant. Where conventional languages use subtyping to allow a caller to supply more specific arguments or a callee to return more general results, Lex uses explicit coercion: if a SanctionsResult needs to inform a ComplianceVerdict computation, the rule author writes the coercion and it appears in the derivation trace. The design cost is verbosity; the gain is auditability. Every type-level operation is visible in the derivation; no structural conversion happens implicitly.
Type inference is bidirectional and limited. Lambda abstractions require annotated domains; let bindings may be annotated or inferred; and branching matches require return types when branches can differ structurally. A full unification-based inference algorithm in the presence of dependent types and effect rows remains open.
4.12 Sanctions Dominance
An ordinary failure verdict is still a returned value that another expression can inspect. A terminal sanctions refusal must stop the return path. The computation type below represents that outcome while retaining the evidence and effects already observed.
Let 0 denote the empty value type. Its computational counterpart F_\rho 0 can refuse or await evidence while returning no value. Sanctions dominance consumes an admitted non-compliance proof and creates an attributable policy refusal:
G |- p : SanctionsNonCompliant(entity) [rho]
------------------------------------------------- (Sanctions-Dominance)
G |- sanctions-dominance(p) : F_rho 0G |- e : F_rho 0 G |- A : Type_i [empty]
------------------------------------------------------ (Abort-Map)
G |- abort(e, A) : F_rho AThe operational definition is \operatorname{bind}(p,v.\operatorname{Refuse}(v)). It evaluates the proof computation first, retaining its effects, refusals, and requests. An admitted proof value v then creates the policy refusal with its authority, source, and request binding. This is a computation of F_\rho 0, with no constructor of 0. An ordinary NonCompliant verdict remains an inhabited data value.
Abort-Map maps the impossible return branch and propagates every refusal, suspension, and prior effect unchanged. Thus it changes the declared return type without producing a value of that type. In the outcome construction of Section 4.2, bind never invokes its continuation on \operatorname{Refuse}(p). A sanctions refusal therefore remains terminal through application, sequencing, and bridge composition.
Policy refusals have no object-language handler. Defeasibility selects among rule outcomes before a refusal is established. An authorized correction creates a separately admitted evaluation against its new evidence and governing rules. It preserves the prior refused execution. Compiler preservation must retain the refusal evidence and prohibit a target handler from converting that refusal into a returned permission.
5. The Admissible Fragment
The full core permits non-terminating execution through Rec, so it cannot supply a terminating evaluator for every program. That observation does not establish undecidability of the separate source conversion \equiv_c, whose rules do not unfold Rec. A complete conversion decision procedure remains open. Unrestricted matches and unfilled holes may leave evaluation without a completed value; they do not by themselves make type checking diverge.
Lex defines admissibility by a decidable check on core syntax. This check selects terms for the normalization and conversion results sought below. Decidable type checking additionally requires match coverage, complete hole-verification evidence, and the open metatheory. Structural equality on syntax is constructive. The following checks state the precise boundaries.
Decidable equality on syntax. The mutually recursive
Term/Branch/Exceptioncarriers admit structural decidable equality.Syntax.vnow definesterm_eq_dec,branch_eq_dec, andexception_eq_decby a mutual structural decision procedure. These procedures supply equality without an equality axiom in the admissibility trusted base.Decidable exhaustiveness of match. The typing rule
T_Matchdoes not structurally enforce that branches cover every constructor of the scrutinee’s inductive type; §5.1’s progress theorem is closed conditional on a Prop specmatch_exhaustiveness_property. The required strengthening ismatch_coverage_property: every value reduct of the scrutinee must be covered by the branch list. Rocq closesmatch_coverage_implies_exhaustivenessandprogress_from_match_coverage : confluence_property -> match_coverage_property -> progress_property; admissibility still must construct that coverage certificate from finite constructor coverage, and confluence remains a separate premise until the diamond closes.Decidable verification of filled holes.
VerifyPCAuth(W, h, v, r, t_check)is total once complete status evidence is admitted for the fill/admission check horizont_check: canonical payload signature check (decidable), quorum check (decidable on the finitecommittee(h)of §4.7), linked-timestamp check (decidable modulo the bulletin oracle), credential non-revocation att_check(decidable on a complete finite status input), delegation-depth bound (decidable against the pack-declaredd_maxof §4.8). The external coverage and comparison evidence remains an oracle obligation. Incomplete preparation produces PendingEvidence before this Boolean verification step.
Under these checks, the admissible fragment accepts:
Var, variable references
Sort, with resolved levels (no level variables)
Lambda, lambda abstractions
Pi, dependent function types, admitted only with the empty latent effect row (the full-calculus
Pi-Formof §4.2 carries a latent row[rho]; the admissible fragment requiresrho = empty)App, application
Annot, type annotations
Let, let bindings
Bounded quantifiers (
forall x : A in C. P(x),exists x : A in C. P(x),exists! x : A in C. P(x), andchoose), whenCis a supplied finite prelude collection value and the predicate is admissible. The admitted decision procedure has empty immediate and latent call rows.Constant, references to names in the global prelude signature
Defeasible, when all sub-terms are admissible
Match, restricted to prelude constructor types (
ComplianceVerdict,Bool,Nat,SanctionsResult,ComplianceTag) with known finite constructor signatures. A finite signature makes branch coverage finite even when the type has infinitely many values, asNatdoes
The admissible fragment rejects the following forms, each for a specific reason:
Rec (general recursion): permits non-terminating execution, so it is excluded from the terminating execution fragment.
Unfilled Hole: an unfilled discretion hole is well typed in the full calculus but carries an unresolved
discretion(auth)effect. The admissible fragment accepts only filled authority decisions.General Sigma/Pair/Proj (dependent pairs): the full calculus types these forms, but the present normalization and conversion argument does not cover them. The bounded existential of Section 4.2 is admitted separately because it elaborates to finite search over an explicit collection.
All modal forms (ModalAt, ModalEventually, ModalAlways, ModalIntro, ModalElim): these forms are well typed in the full calculus. They remain outside the admissible fragment until the modal stratification and normalization theorems close.
Pi_meta: higher-order quantification over rules ranges over the open-ended rule space rather than a finite data collection. Admitting it would require reflection over rule syntax and metadata, which falls outside the bounded-reduction argument.
SanctionsDominance: produces a terminal policy refusal in F_\rho 0. Its general compiler-preservation obligation remains in the full calculus. The bounded executor retains a separate refusal outcome.
PrincipleBalance: graph evaluation is excluded until its result is connected to the list evaluator by a normalization theorem.
Temporal coercions (Lift0, Derive1):
Derive1embeds a pack-relative witness in itsTime_1output. Both forms are conservatively excluded until pack-indexed substitution, normalization, and source-to-target transport are proved. Section 3.3 states the missing commutation theorem.Content-addressed references and Literals: content-addressed references require hash resolution, which is an external effect. Literals are syntactic sugar that the elaborator resolves before admissibility checking. They do not occur in admitted core terms.
The admissibility predicate is a decidable syntactic classification. It excludes recursion, external resolution, unresolved authority effects, and forms whose normalization or transport theorems remain open. A total weak head normal form (WHNF) evaluator and decidable type checker for the resulting full fragment remain theorem obligations; only the flat normalization result is closed.
A type checker compares expressions, while an evaluator performs their operations. These tasks need distinct reduction relations. The distinction matters for exceptions and authority checks, because simplifying syntax must not issue an external act.
Runtime and symbolic reduction. Runtime evaluation uses the labelled relation in Section 4.3 and treats lambdas as values. Pure type conversion uses \longrightarrow_c and \equiv_c from Section 4.2. It simplifies syntax beneath binders and preserves unselected exceptions. Its equality is defined even for neutral terms. Normalization and decidability of that equality remain separate questions. The symbolic relation below gives the wider semantic interpretation its reduction target. Its priority-evaluation rule is distinct from pure conversion. Only the runtime primitive transitions emit effects.
Reduction discipline. The Lex symbolic small-step relation ->_L is the compatible closure of the following head-redex rules, collected here so §9’s adequacy statement has a named target:
beta:
(lam x : A. b) a ->_L b[a/x]zeta:
let x : A := e in b ->_L b[e/x]iota (finite match):
match C_i(xs) return P with ... | C_i(xs) => b_i | ... ->_L b_i[xs]when the scrutinee is in constructor formdefeat:
defeat(defeasible b unless (g_1 => b_1 [p_1] | ... | g_n => b_n [p_n]))(c) ->_L v(c), withv(c)the §7.4 priority-evaluator output: sort firing exceptions by(priority descending, source-position ascending), select the first firing body, and return the base body if none fires. A jurisdiction may instead require equal-priority bodies to compose by verdict meet. That rule defines a different evaluator and needs its own agreement proof.tribunal-open:
open_T evidence(v,p) as (x,q).ereduces tojoin_evidence(p,e[v/x,p/q]). When the continuation returnsevidence(w,n), the result isevidence(w,Cut(p,n)). This rule retains the opened provenance without producing another issued act.tribunal-derive: the runtime checks the reusable rule permit, evaluates the exact typed program on the input, and creates the Computed node defined in Section 4.6. Symbolic reduction can simplify the program syntax but cannot emit authority effects.
tribunal-coerce-id: the identity bridge preserves the carrier and original certificate. Its use still passes any applicable current-action check.
tribunal-coerce-comp: a composite bridge processes the checked recognition path in order. Parenthesization does not change that path. Destination decisions and source acts remain in the receipt. Extensional payload equality does not erase certificate distinctions.
fill:
fill(h, e, w) ->_L ewhenw : PCAuth(auth, h, e, request(h,e))verifies at the fill/admission check timet_checkreevaluate:
reevaluate(derive_1(t_0, w_P), omega) ->_L derive_1(t_0, w_{P’})for the metalevel pack-replay of §3.3sanctions refusal: once its proof is admitted,
sanctions-dominance(p)produces \operatorname{Refuse}(p). Sequencing and Abort-Map propagate this outcome and its observed prefix without invoking a return continuation
The compatible closure lifts ->_L through one congruence rule for each binder position of every constructor, with the parallel relation par in Confluence.v.
The relation must reduce under binders. A weak relation that permits both an outer beta step and reduction of its argument, but does not reduce under binders, is not confluent. The witness
t = App (Lambda T (Lambda T' (App (Var 1) (Var 0))))
(App (Lambda U (Var 0)) (Var 0))has two distinct weak Lambda normal forms: contracting the argument first removes its identity application, while contracting the outer beta first leaves that application inside the frozen lambda body. They have no joint reduct under the weak relation. The binder congruences are therefore necessary. Confluence of the present relation remains open. In the admissible fragment, recursion is excluded, matches range over finite prelude types, and bounded quantifiers range over explicit finite collections. Source conversion is the pure relation \equiv_c of Section 4.2. A normalization-based conversion checker must establish soundness and completeness for that relation using pure reduction \to_c. The wider symbolic relation \to_L also contains institutional and effectful contractions; it is a separate metatheory target. The complete weak-head bound and conversion theorem remain open.
A weak head normal form exposes the outer value or constructor needed for the next check. It need not simplify every subexpression. The following bound covers the stated administrative forms. Extending it to application requires control of substitution size.
Lemma (administrative head reduction is bounded). For the fragment of values, lambdas, annotations, and head lets, PaperMechanization.v closes administrative_whnf_bounded_reduction: every closed well-typed term reaches a weak-head-normal value within term_size(t) + let_depth(t) head steps.
The theorem does not yet cover the full calculus. Its extension requires bounded substitution size for beta, finite match, bounded quantifiers over explicit collections, and stratification and adequacy proofs for the modal, temporal, and discretion forms.
Conjecture (SN-admissible). For every closed admissible well-typed term t : A, every reduction sequence from t terminates (strong normalization).
This is stronger than bounded WHNF reduction: bounded WHNF reduction is a property of one evaluation strategy, while strong normalization is a property of the calculus. The conjecture is open. FlatAdmissibleSN.v proves strong normalization for the flat fragment without Pi-types, modals, recursion, or discretion holes. Decidable type checking for the full admissible fragment still requires the complete WHNF and conversion metatheory. The executable checker terminates by a separate evaluation counter and rejects exhaustion; that behavior is not a proof of completeness.
Mechanization record. Section 4.3 gives a direct-term runtime fragment with value-shape preservation, event-kind containment, and a stateful extension. The complete calculus still requires dependent and indexed representation proofs. Generic union-labelled trees provide separate effect-composition lemmas. PaperMechanization.v carries defeasible_effect_join, effect_monotonicity, finite_observation_event_union_bound, and administrative_whnf_bounded_reduction. Dedicated source files carry the finite-algebra, bridge, and metatheory results classified below. LexCore.v closes decidability of the syntactic admissibility predicate, level non-self-application, forward hole authorization, and temporal lift totality. FlatAdmissibleSN.v closes strong normalization for the flat affine fragment. The classification separates these results from the open full-calculus theorems.
The tracked development carries zero Admitted, no live admit tactic, and no top-level Axiom. Three non-constructive dependencies are named: principle_balancing_terminates (decidability of priority-graph acyclicity) closes classically through Coq’s ClassicalDescription, where a constructive Tarjan or Kosaraju procedure would replace the classical step without changing the statement, and two lemmas in the propagation-graph layer (dm_le_antisym, evaluate_fixed) use functional_extensionality_dep; statements whose proofs transit those call graphs disclose the dependency.
The structural source core has unconditional weakening, typed substitution, and regularity under its generated context formation. Its pure conversion commutes with source shifting and substitution. These statements cover the fourteen constructors of the structural source judgment described in Section 4.2 and carry no confluence premise. The richer execution and indexed-constructor claims remain separate.
Pure source confluence and product compatibility are closed in ProductCompatibility.v. They discharge the product premise of beta_preservation in BetaPreservation.v. For the seven head rules and seven recursive contexts of Section 4.2, BetaTracePreservation.v closes preservation, trace_preservation, and typed_captured_trace. Every finite trace retains its assigned source type in a generated well-formed context and embeds into Repaired.steps. The effect-labelled runtime and lawful exception selection require their separate proofs.
Full admissible-fragment preservation still requires its execution relation, constructor signatures, effect rows, and discretion forms. The progress result retains its confluence and match-coverage premises. The parallel diamond required for confluence and strong normalization beyond the flat affine fragment also remain open. Sequential source substitution supplies one structural ingredient. It does not establish the parallel diamond or full execution preservation. Section 12 states the remaining theorems and their logical dependencies.
5.1 Metatheory: Adequacy of the Two-Layer System
The admissible fragment is paired with the typed bytecode defined in Op: Compliance-Carrying Operations (Lorgat 2026c). Compilation raises three questions: whether it preserves completed verdicts, operational outcomes, and distinctions observable in compliance contexts. Finite verdict-preservation cases are mechanized. The general claims retain the obligations stated below.
The shared structure. Lex and Op meet at three points. They share the compliance-context meet-semilattice (K,\bigwedge_K,\top_K). They share the verdict observable on the embedded Applicable fragment. They also verify the same content-addressed PCAuth witness independently. The general compilation homomorphism, full mixed-axis alignment, and verifier transport remain stated obligations of the schema below.
Let L_adm ⊆ Lex be the admissible fragment defined above, and let [[·]] : L_adm → Op be the compilation sought by this schema. The three claims are:
- (a) Verdict soundness (open theorem; finite cases closed). For every
M ∈ L_admand every well-typed compliance contextctx, if Lex reducesMagainstctxto a verdictv, then Op reduces the compiled bytecode against the compiled context to the same verdictv. The closed evidence currently covers the nine compilation cases recognized byCompilationSoundness.v, the open Op reference model (Lorgat 2026g) (verdict_preservation_*). The universal theorem over everyM ∈ L_admremains open until the compiler coverage lemma maps every checker-accepted Lex constructor into those cases.
Completeness modulo operational outcomes (Conjecture). Fix the source program, context, evidence view, and destination policy. Relate Lex and Op configurations through those same indices. Completed executions preserve their verdict, evidence, and obligation outputs. Suspended executions preserve their indexed continuation and effect budget. A provider timeout or failure corresponds to a typed operational outcome. It supplies no negative legal decision. Exhausting the execution budget, called gas, records an Op resource outcome. Receiving-jurisdiction re-evaluation starts the destination’s indexed query and retains the source result as evidence.
The proposed proof uses a weak simulation with Op metering steps treated as internal transitions. It must cover each compiler constructor, suspension, resumption, provider outcomes, and destination adoption. Subject to an adequate execution budget and eventual completion of required external decisions, every completed supported source computation must have a corresponding target computation. This positive direction preserves the runtime’s useful behavior. The converse relates each observable target result to the source query or its explicitly named operational outcome. Both directions require the actual compiler and adapter relations.
Full abstraction on compliance contexts (Conjecture). For all
M, N ∈ L_adm,MandNproduce the same verdict in every Lex compliance context iff their compilations produce the same verdict in every Op compliance context. The intended proof strategy is a compliance-context simulation relation in the CompCert style (Leroy 2009): build a relationR ⊆ L_adm × Opthat contains the pair(M, [[M]])for every well-typedM, is closed under reduction in both directions, and respects compliance-context observation. The technical content sits in showing that compiling distinct discretion-hole sites preserves observational distinctness, that pack-evolution rewrites do not glue distinct verdict trajectories under compilation, and that tribunal coercions compile to bytecode-level transport that an Op compliance-context observer can distinguish exactly when the Lex observer can. None of these three sub-arguments is reduced to the Lex/Op specifics yet; the present paper claims full abstraction as a conjecture with a proof strategy.
The complete simulation requires a case analysis over the Op semantics and each Lex compilation constructor. The finite verdict-preservation cases support part of that argument. Compiler coverage, indexed suspension, and operational-outcome correspondence remain separate proof obligations. The companion Op development also closes a deliberately finite verdict-agreement theorem in LexOpAdequacy.v, modulo prelude and host_sanctions; the descriptive theorem aliases are lex_op_finite_verdict_agreement and lex_op_finite_verdict_agreement_bisim. This is not Lex denotational adequacy or full abstraction. Modal operators, temporal coercions, pack evolution, unfilled holes, and the compliance-context full-abstraction theorem remain outside the closed finite-case soundness fragment.
Lex specifies what a compliance rule decides; Op specifies how the same decision is computed, metered, and replayed. Nine finite compilation cases close. The universal L_adm source-to-target theorem still requires compiler coverage, and the converse remains conjectural pending the bisimulation and compliance-context proofs.
Op supplies execution metering and dispatch. Lex supplies indexed judgments, effect budgets, and suspended decision computations. Destination adoption evaluates the receiving rule set. The simulation must preserve these interfaces and their distinct outcomes.
Admission must connect the checked source to the exact executable and its evaluation conditions. The digest fields below identify these inputs. Receipts supply the checks required for admission. A receipt for another rule pack or request cannot justify this executable.
Admission carrier at the Lex -> Op boundary. The public boundary object consumed by an admission host is an AdmissionProgram record:
AdmissionProgram = {
op_payload_digest : OpPayloadDigest,
lex_source_digest : LexSourceDigest,
pack_digest : PackDigest,
context_digest : ContextDigest,
compiler_digest : CompilerDigest,
registry_digest : PrimitiveRegistryDigest,
gas_schedule_digest: GasScheduleDigest,
oracle_log_digest : OracleLogDigest,
gas_bound : Nat,
effect_row : EffectRow,
required_receipts : List LexReceipt,
pcauth_entries : List AcceptedFilledHole,
failed_predicates : List SafetyPredicate,
deferred_predicates: List SafetyPredicate
}The admission rule is fail-closed: the Op payload is admitted only if the payload, source, pack, context, compiler, primitive registry, gas schedule, PCAuth entries, oracle log digest, gas bound, and effect row agree with the receipt set and the observed environment. It additionally consumes the exact OperationallyAdmissible witness of Section 7.4 at the named use stage. The smaller accepted predicate checks only unresolved-set emptiness. The closed receipt algebra proves locality for that projected component: composing accepted receipts cannot hide unresolved obligations or discretionary frontiers. The Rocq carrier AdmissionEnvelope.v closes the structural admission facts: admission_fails_closed_on_payload_mismatch, admission_fails_closed_on_unaccepted_receipts, admission_no_failed_or_deferred_predicates, admission_pcauth_entries_verified, and receipt_to_bundle_preservation.
The executable Op checker enforces the same interface at the payload level: initializers match their annotations, declared outputs return the stated type, and finite matches are exhaustive with type-consistent arms. Lex lowering emits a typed unreachable catch-all. The open proof-bundle theorem must show that compilation preserves the obligation frontier, PCAuth request bindings, gas and effect bounds, and the context digest. Lex compiles to an Op payload plus an admission envelope, and the envelope type-checks only for the activity authorized by the Lex proof.
Mechanization Boundaries
The table identifies the mathematical models supporting the principal statements. A closed model theorem and a compiler-refinement theorem are separate results. Q means a non-vacuous Rocq theorem closed with Qed. C means a Rocq theorem whose named proposition premises remain open. O means a named open proposition or a manuscript proof not represented by a Rocq theorem. J marks a conjecture.
| # | Statement | Section | Class | Rocq result or boundary |
|---|---|---|---|---|
| 1 | Re-evaluation is functorial | 3.3 | Q | PackReevaluation.v: src_0_reevaluate, reevaluate_id, reevaluate_compose, rewrite_effective_date_preserved |
| 2 | Pack-evolution soundness, stable fragment | 3.3 | O | Manuscript induction; no Rocq theorem |
| 3 | Pack-evolution soundness, modal/temporal subsystem | 3.3 | J | Conjecture in the body |
| 4 | Temporal rule-graph non-regression | 3.2 | Q | TemporalStratification.v: no_time1_premise_to_time0_rule, temporal_non_regression, no_temporal_retract |
| 5 | Finite discretion-hole event-union bound | 3.5 | Q | PaperMechanization.v: finite_observation_event_union_bound; the cryptographic instantiation remains open |
| 6 | Quorum acceptance unfolding | 3.5 | Q | PCAuthQuorum.v: quorum_acceptance_unfolding and its policy, payload, chain, anchor, and revocation lemmas |
| 7 | PCAuth forgery reduction | 3.5 | O | Manuscript EUF-CMA reduction; no Rocq theorem |
| 8 | Prop erasure | 4.1 | O | Manuscript induction; no Rocq theorem |
| 9 | Effective finite decision and choice | 4.2 | O | Constructive finite algorithms in the body. Supporting list decisions and witness extraction are mechanized in FiniteDecisions.v; the effective-domain interface requires its own refinement |
| 10 | Constructive finite choice | 4.2 | O | Explicit decision-indexed table construction and finite call bound; runtime refinement remains open |
| 11 | Immediate and runtime effect containment | 4.3 | O | Direct-term runtime-shape, event-kind, and stateful results in ActualEffects.v and ActualState.v; dependent, indexed, and full-constructor refinement remains open |
| 12 | Defeasible effect join | 4.4 | Q | PaperMechanization.v: defeasible_effect_join |
| 13 | Issued-act provenance and derived evidence | 4.6 | O | Actual-transition proof construction; admission, substitution, and compiler-preservation lemmas required |
| 14 | Abstract function-bridge laws | 4.6 | Q | BridgeSemantics.v: equivalence, composition, congruence, and strict function-target coherence |
| 15 | Runtime bridge interpretation | 4.6 | O | Interpreter construction and proof in the body; actual-syntax, latent-effect, certificate, and projection lemmas required |
| 16 | Finite authority recognition is decidable | 4.6 | O | Manuscript fixed-point proof; no Rocq theorem |
| 17 | Delegation does not expand authority | 4.7 | O | Manuscript induction; no Rocq theorem |
| 18 | Delegation soundness | 4.8 | O | Manuscript induction; no Rocq theorem |
| 19 | Revocation determinism | 4.9 | O | Manuscript proof from bulletin order; no Rocq theorem |
| 20 | Administrative head reduction is bounded | 5 | Q | PaperMechanization.v: administrative_whnf_bounded_reduction for the stated fragment |
| 21 | Strong normalization of the admissible fragment | 5 | J | Flat fragment closed in FlatAdmissibleSN.v; full claim is conjectural |
| 22 | ComplianceVerdict is a Heyting algebra |
7.4 | Q | VerdictHeyting.v: thirteen laws bundled in verdict_is_heyting |
| 23 | Receipt locality | 7.4 | O | Rich keyed-map construction in the body. Projected equations are closed in ReceiptAlgebra.v: accepted_compose_iff, compliant_compose_iff, admission_locality |
| 24 | Admission envelope fails closed and preserves receipts | 5.1 | Q | AdmissionEnvelope.v: five named structural admission theorems |
| 25 | Priority evaluator agreement | 7.4 | Q | DefeasibilityPriority.v: eval_defeasible_normalized_meet |
| 26 | Pack-rewrite preservation | 7.4 | O | Manuscript proof sketch; no Rocq theorem |
| 27 | Adequacy of the presheaf model | 9 | O | Per-constructor obligations are stated; full mechanization is open |
| 28 | Full derivational cut elimination | 9 | O | Requires explicit Cut syntax, principal and commuting conversions, coverage, preservation, and normalization; principal program normality is separately conditional |
| 29 | Source-core weakening | 4.2 | Q | Generalized insertion and formed branch telescopes for all fourteen source typing constructors |
| 30 | Progress | 5 | C | Closed under confluence_property and the match-coverage certificate |
| 31 | Full operational preservation | 5 | O | Remaining execution rules, effect typing, and institutional semantics |
| 32 | Symbolic execution confluence | 5 | O | Named metatheorem through the open par_diamond_spec |
| 33 | Source-core substitution | 4.2 | Q | Typed dependent substitution on source syntax with pure conversion and formed targets |
| 34 | Source-core regularity | 4.2 | Q | Every derived source type has a universe in a generated well-formed context |
| 35 | Pure source confluence and product compatibility | 4.2 | Q | ProductCompatibility.v: source_steps_confluent and pi_convertible_decomposition; no termination claim |
| 36 | Source trace preservation | 4.2 | Q | BetaTracePreservation.v: trace_preservation. Seven head rules and seven recursive contexts retain arbitrary assigned types under generated context formation |
A closure label applies to the named model and its assumptions. It supplies no additional constructor coverage or implementation relation. The following constructions have manuscript proofs: sound Boolean calculation, local-permission preservation, extension locality, exclusion conservation, historical reproducibility, and replay separation. Their proofs identify concrete algorithms and retained indices. Their compiler refinements remain separate obligations.
Theorem-to-code relation. An implementation connection consists of a source syntax representation, a code function, and a relation between their inputs and outcomes. The relation includes effects, certificates, suspended continuations, and typed errors. A theorem constrains a code path only after its preconditions and result relation are established for that path. Matching names or finite examples is insufficient.
ActualEffects.vandActualState.vuse the capturedLex.Syntax.Term. An executable projection maps ten Rust constructor families into that representation. Nine exact abstract syntax tree (AST) instances have compiled representation equalities and matching observations. A universal source-to-runtime relation must also cover the dependent checker, exact effect indices, and remaining constructors. The separate generic-tree result remains a support lemma.The owning paths are
typecheck::inferandtypecheck::check, followed by an explicit backend lowering.evaluate::evaluateis a typed-AST demonstration runner. Production predicate authorization usespredicate_runtime::evaluateon closedLexPropositionvalues. Their source lowering must preserve the actual verdict, immediate and latent effects, store, and continuation observations of Section 4.3.PaperMechanization.v’s administrativeWhnfTermhas heads, lambdas, annotations, and lets. It has neither variables nor applications;closedandadmissibleare constant true on that carrier. Its bound concerns those administrative constructors.typecheck::whnfrequires a distinct simulation covering substitution, application, matching, fuel, and its error outcomes.BoundedQuantifiers.vandFiniteDecisions.vconcern explicit finite domains and supplied predicate decisions.decide::finite_domain_checkand the bounded search paths require representation, coverage, decision-correctness, and timeout relations. Totality of an arbitrary external predicate is not an implicit premise of the runtime.VerdictHeyting.vproves the five-state scalar algebra.compose::verdict_meetandcompose::compose_fiber_resultsrequire a representation that retains exemption and applicability evidence. The inspectedlex-corescalar has three constructors. The richerFiberResultand permission contract therefore require an explicit data and serialization extension, with compatibility rules.ReceiptAlgebra.vproves the projected receipt equations.AdmissionEnvelope.vproves structural checks on its record. The admission host must relate these to complete keyed fibers, current-use authority, and the atomic recording of its admitted transition. The projectedacceptedpredicate supplies no execution capability.BridgeSemantics.vconcerns an abstract total-function target. The bridge interpreter must preserve rejection, suspension, ordered checks, and certificate identity. A completed-payload projection is only one component of that refinement.PackReevaluation.vand the temporal rule graph preserve their stated source projections.temporal::infer_temporal_sort, re-evaluation, and the history host must additionally implement qualified interval unions and the bitemporal query contract.
For each relation, a code identity includes the repository commit, exact source hashes, compiler and dependency identities, and the function signature. A working-tree source is identified by its own hash, rather than by the commit alone. The inspected lex-core package declares version 0.1.0 and Rust 1.93. Reproduction requires its exact source identity and the formal-file identities in an accessible immutable archive; Section 11 records that outstanding requirement. No source-to-compiler or compiler-to-admission-host refinement is inferred from this package version. The Lex and admission-host developments must prove those relations on their actual functions. The positive objective is that supported programs realize the specified outcomes, as well as preserving their safety invariants.
Finite compiler soundness (direction (a) of the §5.1 adequacy claim, mechanized in CompilationSoundness.v (Lorgat 2026g) across nine verdict_preservation_* cases) is not a Lex paper-level statement and is therefore not in the table; it is the source for the §5.1 claim that direction (a) is closed on those cases. The underlying context, substitution-commutation, well-scopedness, and relation-alignment lemmas support the paper-level statements. Their exact source and semantic relations determine their scope.
6. The Prelude
The core rules describe how expressions combine. They also need a shared vocabulary for company data, verdicts, and field access. The prelude fixes those constructors and accessor types. A jurisdictional pack supplies rules expressed in that vocabulary.
The admissible fragment operates within a compliance prelude: a global signature providing the type vocabulary for jurisdictional rules. The prelude is organized into:
Core types:
IncorporationContext,ComplianceVerdict,SanctionsResult,Bool,Nat,ComplianceTag, and finite collection families such asCollection(T),List(T),Set(T), andMultiset(T).Verdict constructors:
NonCompliant,Pending,NotApplicable,Exempt,Compliant.ComplianceVerdictis a bounded five-element chain ordered by legal restrictiveness, with the order, the meet/join semantics, and the Heyting structure proved in Section 7.4.Boolean constructors:
True,False.Sanctions constructors:
Clearplus thesanctions_queryeffect.Tag constructors and accessors: jurisdiction-specific enumerated values (e.g.,
FullLicense,InPrincipleApproval,FitAndProperSatisfied) together with the field projections that extract them from anIncorporationContext(e.g.,fsra_authorization_status,director_count).Collection combinators: enumeration, membership proofs,
filter, and cardinality|C|for finite-collection quantification and threshold rules.Boolean, numeric, and sanctions accessors, and explicit combinators for threshold and predicate operations.
Agreement on names alone does not establish agreement on accessor meaning. An accessor for appointment status must have the same declared interpretation wherever a rule using it executes.
All prelude types live at universe level 0. The prelude is the vocabulary within which the admissible fragment operates; it is versioned per release of the logic. A rule authored against one prelude version is portable across implementations that agree on that version.
7. Worked Examples
The examples now combine the constructions. The British Virgin Islands (BVI) appointment rule shows why an exception must preserve a separate deadline duty. The authority examples add judgment and recognition. Accounts filing and limitation periods show how later evidence changes an assessment while retaining its historical inputs.
The examples span both the admissible fragment and the full calculus. Four have mechanized counterparts: sanctions hard block (SanctionsHardBlock.v), fit-and-proper lifecycle (ADGMFitAndProper.v), hypothetical ADGM-DIFC mutual recognition (ADGMDIFCMutualRecognition.v), and Pakistan deadline tolling (PakistanDirectorsReportTolling.v). The Seychelles reading, BVI rule, and UK accounts rule are proved only at manuscript level. The mechanical BVI rule body of Section 7.1 and the scalar verdict operations of Section 7.4 lie in the current admissible fragment. The evidence carriers and admission records in Section 7.4 have the additional contracts stated there. Sections 7.2, 7.3, and 7.5 through 7.8 use full-calculus features. The executable checker handles the mechanical sanctions path through its runtime preflight; sanctions_query and Sanctions-Dominance remain full-calculus constructs.
7.1 Defeasible Rule: BVI Minimum Directors
The BVI Business Companies Act separates minimum-director coverage from the registered agent’s first-appointment duty. Section 109(4A) provides the pre-appointment exception. Section 113(1), as substituted by section 21 of the 2024 Amendment Act, requires appointment within 15 days after incorporation. The amendment commenced on 2 January 2025. The earlier six-month rule belongs to the historical pack. 1
A deadline duty and an exception have different meanings. The following illustrative encoding keeps them as distinct rule instances. The pack supplies the applicable deadline and calendar interpretation. Complete registry evidence supplies first_appointment_absent.
The absence test uses a complete registry view. An unresolved query supplies no absence witness. Evidence acquisition must finish before this pure rule receives its context.
minimum : Pi(ctx:IncorporationContext)[empty].ComplianceVerdict :=
lam(ctx:IncorporationContext).
defeasible
(if ctx.director_count = 0 then NonCompliant else Compliant)
unless
(guard: ctx.first_appointment_absent,
body: NotApplicable, priority: 1)
endappointment : Pi(ctx:IncorporationContext)[empty].ComplianceVerdict :=
lam(ctx:IncorporationContext).
if ctx.first_appointed_by ctx.first_appointment_deadline
then Compliant
else if ctx.event_time <= ctx.first_appointment_deadline
then Compliant else NonCompliantThe first body and its exception both have type ComplianceVerdict. The guard has type Bool. if b then x else y abbreviates an exhaustive Boolean match. The defeasible form abbreviates the core node with its explicit (g,b,p) exception. Lambda construction is pure. Each displayed body has empty row, so its function has empty latent row. A Boolean-only exception fails the required result-type agreement.
A fiber records one rule’s result for one entity and compliance domain. This example has two fibers because the minimum-director rule and appointment duty can have different outcomes. Section 7.4 defines their composition.
Before appointment, the minimum-director fiber records NotApplicable. The appointment fiber records the live duty and its deadline. Before it falls due, its current-time check passes while its future obligation remains open. After that deadline, an absent appointment produces NonCompliant, even if the first fiber retains its exception. An appointment made on time supplies a positive witness. A late appointment records current directors while preserving the earlier missed duty. It does not silently discharge that historical obligation.
The language can also express a bounded exception through start <= event_time < end. Its endpoint is part of the rule, not inferred from an absent registry entry. Current deployment requires the selected law, commencement conditions, complete registry coverage, and the responsible legal interpretation. The two-fiber construction preserves the statutory distinction instead of asserting that s.109(4A) itself states a deadline.
7.2 Cross-Jurisdictional Rule with Dependent Types
Selecting a jurisdiction also selects the available entity fields. The match therefore returns a function whose argument type is the context for that jurisdiction. This dependent result lies outside the current admissible fragment’s flat matching discipline. For this example, Jurisdiction is the two-constructor type ADGM | Seychelles, so the displayed match is exhaustive. Let rho = {discretion(ADGM.FSRA)}. Both returned functions have this common latent row; effect weakening admits the pure Seychelles body at that row. The motive binds k, and the selected function is applied to the already supplied ctx:
lambda (j : Jurisdiction).
lambda (ctx : EntityContext j).
(match j return k. (Pi(_ : EntityContext k)[rho]. ComplianceVerdict) with
| ADGM => lambda (c : EntityContext ADGM) [rho].
match c.fit_and_proper_status return ComplianceVerdict with
| FitAndProperSatisfied => Compliant
| FitAndProperUnderReview => Pending
| _ => ?fp_adgm : ComplianceVerdict
@ authority ADGM.FSRA
scope { jurisdiction: ADGM }
| Seychelles => lambda (c : EntityContext Seychelles) [rho].
match c.has_director_appointed_under_act return ComplianceVerdict with
| True => Compliant
| False => NonCompliant) ctxHere, EntityContext is a type family indexed by jurisdiction. The context for an ADGM entity carries fields specific to ADGM (FSRA authorization status, fit-and-proper assessments). The context for a Seychelles entity carries fields specific to Seychelles (whether any director holds an appointment made under the Act, under s.130(1) of the Act read in Section 4.2). The return type of the outer match depends on the jurisdiction, it is Pi(_ : EntityContext j)[rho]. ComplianceVerdict, where j is bound by the outer lambda. Applying that function to ctx returns ComplianceVerdict with effects bounded by rho.
The ADGM branch contains a typed discretion hole ?fp_adgm: when the fit-and-proper status is neither satisfied nor under review, the machine cannot determine compliance. A judgment of type ComplianceVerdict must be supplied by the ADGM FSRA. The Seychelles branch has no discretion hole: has_director_appointed_under_act is the Boolean the s.130(1) bounded existential of Section 4.2 decides, and appointment under the Act is a binary fact of record.
The displayed rule places jurisdiction dependence and required judgment directly in its type. Comparison with another language must distinguish a native construct from an encoding, as Section 10 does. The dependent type ensures that an ADGM-specific accessor is never applied to a Seychelles context, and vice versa. The discretion hole ensures that the “fit and proper” determination is not silently approximated.
7.3 Sanctions Hard-Block
The example represents screening under a selected Seychelles sanctions rule pack. The pack determines the subjects, applicable designations, licenses, exemptions, and evidence requirements. It does not treat an unresolved name match as an admitted violation.
Fix the selected list, version, and evidence view for each screening obligation. Clearance and violation evidence carry these same indices. Write \operatorname{Clearance}(e,\ell,v,\omega) for the pack’s admitted clearance evidence for subject e, list \ell, version v, and view \omega. Its violation alternative is the SanctionsNonCompliant(e) record with those list and as-of indices. The notation below suppresses these fixed indices. Assume a screening interface for each required subject e: screen(e) has computation type F_{[\mathtt{sanctions\_query}]}\operatorname{ScreenDecision}(e). Its returned decision is either ScreenClear(q), carrying admitted clearance evidence under that pack, or ScreenViolation(p), carrying p : SanctionsNonCompliant(e). A missing response or unresolved match suspends as a typed request. The interface may return a decision only after checking the applicable authority, list version, scope, and as-of evidence. This is an explicit interface premise, not a deduction from a scalar verdict.
Let Unit : Type_0 be the one-constructor prelude data type with unit : Unit. It records successful completion of a screening obligation without adding a verdict. The following computation notation uses return, bind, and the terminal refusal rules of Sections 4.2 and 4.12. The finite list required_subjects(ctx) includes the incorporator, directors, and beneficial owners selected by the pack. sequence is the finite left-to-right fold of bind; it retains all prior effects.
check_subject(e) :=
bind(screen(e), decision.
match decision return F_[sanctions_query] Unit with
| ScreenClear(q) => return unit
| ScreenViolation(p) => abort(sanctions-dominance(p), Unit))
check_entity(ctx) :=
bind(sequence(map check_subject (required_subjects(ctx))), _.
return Compliant)Sanctions-Dominance converts the admitted violation proof to a computation returning no value. Abort-Map changes its declared return type to Unit while retaining the refusal. Bind therefore cannot reach the final Compliant return after a violation. If every required subject supplies clearance evidence, the finite sequence completes and returns Compliant. A suspension leaves the entity check unresolved. These are three distinct operational outcomes.
An ordinary NonCompliant verdict remains reportable data. Terminal refusal follows from the admitted proof and dominance rule. Lawful licenses, exemptions, delisting evidence, and shared-authority recognition are assessed before that proof is admitted. Ordinary defeasibility cannot handle a refusal once dominance has fired.
The computation retains the distinguished sanctions_query effect. A full-calculus caller must budget that effect. Executable preflight must implement the same proof-bearing screening contract and preserve its refusal and suspension outcomes; a Boolean or five-value verdict alone is insufficient evidence of that preservation.
7.4 Verdict Lattice
An entity is subject to several rules, often from several statutes. A fiber is one rule applied to one entity, producing a ComplianceVerdict for one compliance domain. Fix the finite domain set D and the five-element verdict chain V below. Evaluation against a rule pack yields a partial function s : D’ -> V. Here D'\subseteq D contains the domains with evaluated summaries. An absent entry supplies no OutsideScope witness.
Results within one domain compose by Heyting meet. How Compliance Composes (Lorgat 2026b) defines aggregation across domains. A pack is the versioned set of rules active in one jurisdiction at an event time.
The carrier is the bounded five-element set \mathcal{V} = \{ \mathtt{NonCompliant}, \mathtt{Pending}, \mathtt{NotApplicable}, \mathtt{Exempt}, \mathtt{Compliant} \} with the total order \mathtt{NonCompliant} < \mathtt{Pending} < \mathtt{NotApplicable} < \mathtt{Exempt} < \mathtt{Compliant}.
The chain orders a scalar display summary. Each fiber also retains its applicability evidence and exact rule instance:
NonCompliant: a hard fail.Pending: the rule is live but a required check has not yet been disposed.NotApplicable: the rule does not reach this entity.Exempt: the rule reaches the entity but a statutory exemption defeats the obligation.Compliant: the rule applies and is satisfied.
The passing states are exactly those strictly above Pending: {NotApplicable, Exempt, Compliant}. The scalar is a useful algebraic summary. The authoritative evaluation record retains a map of rule instances to their individual results. The same scalar can summarize different applicability histories. For example, Exempt with NotApplicable and a lone NotApplicable have the same meet but different witnesses. Permission and cross-jurisdiction transport use the retained map.
Lex composes verdicts with the lattice operations on this chain:
verdict_meet(a, b) = min(a, b) -- restrictive composition
verdict_join(a, b) = max(a, b) -- permissive compositionverdict_meet is used for conjunctive composition: every fiber in a domain must clear the bar, so the most restrictive verdict wins. verdict_join is used for disjunctive composition: if any one of a family of sub-rules is an alternative under the same admitted local rule, the summary takes its largest value. The rule supplies the alternative-licensing proof. A join across unrelated rules cannot create action authority. The lattice facts used below are standard finite-chain facts in the sense of Birkhoff’s Lattice Theory; the Heyting-algebra reading is the standard locale-theoretic one in Johnstone’s Stone Spaces.
For all a, b, c \in \mathcal{V}, the operations satisfy:
Idempotence: a \wedge a = a and a \vee a = a.
Commutativity: a \wedge b = b \wedge a and a \vee b = b \vee a.
Associativity: (a \wedge b) \wedge c = a \wedge (b \wedge c) and (a \vee b) \vee c = a \vee (b \vee c).
Absorption: a \wedge (a \vee b) = a and a \vee (a \wedge b) = a.
Distributivity: a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c) and a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c).
Boundedness: \bot = \mathtt{NonCompliant} and \top = \mathtt{Compliant}, so \bot \wedge a = \bot and \top \vee a = \top.
These identities follow from totality and the definitions \wedge = \min and \vee = \max. For distributivity, assume without loss of generality that b \leq c. Then b \vee c = c and b \wedge c = b. Also a \wedge b \leq a \wedge c and a \vee b \leq a \vee c, so a \wedge (b \vee c) = a \wedge c = (a \wedge b) \vee (a \wedge c) and a \vee (b \wedge c) = a \vee b = (a \vee b) \wedge (a \vee c). The dual case c \leq b is symmetric.
Implication answers a question about scalar composition: which summaries can meet with a and remain at most b? For example, Compliant implies Pending with scalar result Pending. This calculation concerns the verdict order. Permission still requires the rule witnesses defined below.
Theorem (ComplianceVerdict is a Heyting algebra). Define implication on \mathcal{V} by a \Rightarrow b = \begin{cases} \top & \text{if } a \leq b, \\ b & \text{if } b < a. \end{cases} Then for every x, a, b \in \mathcal{V}, x \leq (a \Rightarrow b) \quad\Longleftrightarrow\quad x \wedge a \leq b. Hence \mathcal{V} is a bounded distributive lattice with relative pseudocomplements, therefore a Heyting algebra. In particular, a \wedge (a \Rightarrow b) = a \wedge b. The pseudocomplement is \neg a := (a \Rightarrow \bot).
Proof sketch. If a \leq b, then a \Rightarrow b = \top. The left side is always true, and the right side holds because x \wedge a \leq a \leq b. If b < a, then a \Rightarrow b = b. Since \mathcal{V} is totally ordered, x \wedge a \leq b holds exactly when x \leq b, which is exactly the left side. This is the residuation law. The preceding proposition supplies bounded distributivity, so the relative pseudocomplements make \mathcal{V} a Heyting algebra. The identity a \wedge (a \Rightarrow b) = a \wedge b is the same two-case analysis: if a \leq b, both sides are a; if b < a, both sides are b.
The Seychelles IBC Act 2016 and the Seychelles AML Act 2020 impose rules in the same compliance domain. Lex composes their fibers with verdict_meet, so the more restrictive verdict controls. On Applicable fibers this agrees with the meet in How Compliance Composes. That paper keeps mixed applicability separate rather than using this scalar chain as its provenance record.
In Section 7.1, NotApplicable identifies the minimum-director exception, while the appointment deadline remains a separate duty. A scalar summary cannot retain that distinction. The following record keeps each rule instance and its evidence.
Rule records and permission. Fix an evaluation key k=(j,a,q,L,\tau): jurisdiction, action, immutable request, rule pack, and the temporal context of Section 4.9. A complete selector identifies the finite required rule-instance set I_k. It includes the policy roots, range queries, and absence predicates used to select those rules. A FiberResult(k,i) retains the verdict, applicability witness, source acts, derivation, and outstanding obligations for instance i.
Its passing witness is one of:
Satisfied(rule,applicability,proof)
Exemption(rule,legal_basis,scope,proof)
OutsideScope(rule,scope,proof)A passing label without its checked witness has no admission meaning. A complete record M maps every i\in I_k to its result. A domain summary includes both the scalar meet and the sets of applicable, exempt, and out-of-scope rule identifiers. Mixed applicability remains explicit. Projection to the richer carrier of How Compliance Composes starts from those fibers, before any scalar fold. An ADGM authorization result of Compliant and a capital result of Pending therefore retain both records and summarize as Pending.
An evaluation has three distinct results. EvaluationComplete certifies that the declared evaluator has returned its typed report. It can report non-compliance or a terminal Pending verdict. A suspended evaluator instead returns Await with its frontier. LegallyAllowed carries positive local justification for the exact action. OperationallyAdmissible additionally carries the resources and current authority required at the named use stage.
LegallyAllowed(k,R) :=
CompleteCoverage(k,R.rules)
and every required fiber has its checked passing witness
and all obligations due for this action are discharged
and all judgments required for this action are resolved
and current_local_decision(k) = Allow
OperationallyAdmissible(k,R,S) :=
LegallyAllowed(k,R)
and CurrentAuthority(k,S) and ExactRequest(k,S)
and RequiredReservations(k,S) and ProtocolReady(k,S)
and FreshAtNamedUseStage(k,S)The three carriers have different constructors. A complete evaluator receipt cannot be cast to either permission type. Continuing obligations remain in the state even when they are not due for this action. Operational admission checks all mutable guards within the transaction that records the admitted transition. Dispatch or provider acceptance requires its own current check when the institutional authority contract names that later stage.
Proposition (permission preserves local decisions). If OperationallyAdmissible(k,R,S) is inhabited, the local decision for k is Allow, and every required fiber has a passing witness. Importing evidence or taking a scalar join cannot turn a reserved Refuse record into such an inhabitant.
Proof. Eliminate the operational constructor, then the legal constructor. Their fields supply the local Allow equality and every fiber witness. Recognition adds source and receiving receipts to M. It has no constructor for the destination’s current local record. A Refuse equality contradicts the required Allow equality. \square
Useful recognition follows through the same constructors. Suppose a receiving rule accepts a foreign identity attestation for its identity obligation. A checked bridge discharges that fiber while retaining the original act. The destination’s remaining checks and local decision then construct its legal permission. Identity collection need not run again. An independent second rule can use the same attestation under its own permitted scope and exact request binding.
Authority-indexed results. A carrier [T]VerdictIs(v) contains issued or derived evidence under T, as in Section 4.6. Two results can enter a common tribunal U through explicit bridges. A reusable U rule permit may then compute their meet and a derived certificate. Its certificate retains both source acts and recognition paths. This calculation creates no fresh issued act and supplies no substitute for U’s reserved local decision.
Receipt composition. Write R=(k,I,M,v,O,U,F), with exact key, covered rule set, fiber map, scalar summary, declared obligations, unresolved obligations, and unresolved judgments. Two receipts are compatible when their keys agree and overlapping fiber and obligation identifiers have the same exact contents. Compose compatible receipts by map union, scalar meet, and set union. Conflicting records produce an explicit reconciliation result. They cannot be silently overwritten.
The receipt equations use only scalar meet and outstanding-set unions. Isolating those fields gives a smaller algebra that can be checked independently. It omits the action, selector, and individual rule evidence, so its readiness predicate cannot replace permission.
The smaller carrier R_0=(v,O,U,F) remains a useful projection. Define ready(R_0) by U=F=\emptyset, and strict(R_0) by ready(R_0)\land v=\mathtt{Compliant}. These are the predicates named accepted and compliant in ReceiptAlgebra.v. They describe the projected record. strict deliberately excludes exemption and out-of-scope fibers. It is not the definition of LegallyAllowed.
Theorem (receipt locality). For compatible receipts, ready(R_1\otimes R_2)\iff ready(R_1)\land ready(R_2), strict(R_1\otimes R_2)\iff strict(R_1)\land strict(R_2). Every original fiber remains in the union. For a complete selected conjunction, all required fibers pass exactly when each selected fiber has a passing witness.
Proof. A union is empty exactly when both operands are empty. The meet of two chain elements is top exactly when both are top. Compatible map union retains every key and its exact result. The final equivalence is finite universal introduction and elimination. The local decision and current authority are separate premises for legal and operational admission. The existing accepted_compose_iff and compliant_compose_iff prove the two projected equations. A refinement to the richer receipt must also preserve its keys, selector, map, and witnesses. \square
Consider the BVI rule before any director has been appointed. With the exception guard true, normalization assigns Compliant to the inactive base clause and NotApplicable to the exception. Their meet returns NotApplicable. Meeting the original bodies would retain the base body’s NonCompliant result. Normalization must express priority selection before taking the meet.
Strict-priority premise. The proposition below assumes p_1 > \cdots > p_n > p_0. The admissible fragment total-orders exceptions by (priority, source-position). Equal numeric priorities therefore do not trigger a meet: the first source position wins after sorting. A rule that composes tied bodies by verdict meet defines a different evaluator and requires a separate agreement theorem.
Proposition (priority evaluator agreement). Let a defeasible rule have base body b_0 and exceptions (g_1, b_1, p_1), \ldots, (g_n, b_n, p_n) ordered by descending priority p_1 > \cdots > p_n > p_0. For a context c, define \nu_i(c) = \begin{cases} b_i(c) & \text{if } g_i(c)=\mathtt{True} \text{ and } g_j(c)=\mathtt{False} \text{ for all } j < i, \\ \top & \text{otherwise,} \end{cases} and \nu_0(c) = \begin{cases} b_0(c) & \text{if } g_i(c)=\mathtt{False} \text{ for all } i, \\ \top & \text{otherwise.} \end{cases} Then \mathrm{defeat}(r)(c) = \nu_0(c) \wedge \nu_1(c) \wedge \cdots \wedge \nu_n(c).
Proof sketch. Exactly one normalized clause contributes the selected body’s value, which may itself be \top. If some exception guard is true, let k be the least index with g_k(c)=\mathtt{True}; then \nu_k(c)=b_k(c) and every other \nu_i(c)=\top. If no exception guard is true, then \nu_0(c)=b_0(c) and every exception clause is \top. Since \top=\mathtt{Compliant} is the identity for meet, the meet of the normalized family returns exactly the verdict selected by the priority evaluator.
A changed rule pack raises a different preservation question. Two packs can derive different appointment deadlines from the same incorporation event. The next obligation retains both derivation records, including when their verdicts differ.
Open obligation (pack-rewrite preservation). Let P \rightarrow P' be a pack evolution witness. If a Time_1 verdict derivation under P produces \delta : P \vdash e \Downarrow (t, v), then re-evaluation under P' produces a fresh derivation \delta' : P' \vdash e \Downarrow (t', v') such that the semantic history is additive: \mathrm{History}' = \mathrm{History} \cup \{(P, t, v, \delta), (P', t', v', \delta')\}. The old verdict is preserved as the frozen historical derivation under P; the new verdict is a distinct Time_1 derivation under P'. No rule overwrites (P, t, v, \delta) with (P', t', v', \delta').
Required proof. Re-evaluation must consume the same Time_0 facts together with a new pack witness, producing a new derived judgment rather than mutating the old one. The proof must show that temporal stratification blocks any retraction from Time_1 back into frozen history and that pack evolution is append-only.
7.6 Case study: ADGM–DIFC commit
Fix an illustrative corridor pack. Its sanctions-list selections and reporting window are inputs to this example. The recognition bridge is hypothetical and requires the authority evidence described below.
This case study fixes a single corridor event: an ADGM-licensed asset manager commits a sanctions-screened transaction with a DIFC counterparty. The companion Op paper defines typed bytecode, bilateral signed commitment, and the boundary between operational results and provider outcome evidence (Lorgat 2026c). The present concern is the Lex layer: which obligations are mechanical, which remain jurisdiction-indexed, and exactly where human judgment enters.
The selected pack includes lists from the United States Office of Foreign Assets Control (OFAC) and the United Nations (UN). These list selections are illustrative inputs. The two jurisdictions do not share a single sanctions predicate. The ADGM side screens against OFAC plus the ADGM list; the DIFC side screens against the UN consolidated list plus the DIFC list. Each rule is local and fail-closed:
let adgm_sanctions =
lambda (tx : CorridorTx ADGM) [sanctions_query].
check_lists(tx.counterparty, [OFAC, ADGM_List])
let difc_sanctions =
lambda (tx : CorridorTx DIFC) [sanctions_query].
check_lists(tx.counterparty, [UN_List, DIFC_List])Here check_lists instantiates Section 7.3’s finite bind sequence with subject-and-list-indexed screening evidence. It returns Compliant only after every selected list supplies admitted clearance evidence, propagates unresolved checks as Await, and maps any admitted violation proof through sanctions dominance.
Sanctions mutual recognition is therefore not a coercion rule. Each side must evaluate its own lists; the bridge can only transport agreement once both local checks have passed.
The know-your-customer (KYC) layer contains the determinations that require authorized judgment:
?fit_and_proper_adgm : ComplianceVerdict
@ authority ADGM.FSRA
scope { jurisdiction: ADGM, role: AssetManager }
?approved_person_difc : ComplianceVerdict
@ authority DIFC.DFSA
scope { jurisdiction: DIFC, role: Counterparty }The first hole marks the ADGM “fit and proper” judgment; the second marks the DIFC “approved person” judgment. Neither hole can be discharged by the other jurisdiction. Each requires a local PCAuth witness naming the authority, scope, digest, and timestamp of the fill.
Reporting follows the commit event. At commitment, the receipt retains that requirement as a continuing obligation under Section 7.4. The following fiber checks its later performance.
The reporting obligation is mechanical again. Once the commit event tx.commit_time is fixed as Time_0, the corridor pack derives a legal deadline in Time_1:
let report_deadline : Time_1 =
derive_1(tx.commit_time,
corridor_reporting_window {
pack: corridor_pack,
period: 1_business_day
}) in
match (tx.adgm_report_filed_by report_deadline,
tx.difc_report_filed_by report_deadline)
return ComplianceVerdict with
| (True, True) => Compliant
| _ => NonCompliantThe deadline is a derived legal consequence of a fixed historical event.
Let CommitReady(tx_id) be the proposition that the transaction may be committed. ADGM and DIFC derive it under their own admitted local rules. Each result retains the local sanctions evidence, PCAuth judgment, rule permit, and exact transaction context. The MutualRecognition bridge below is hypothetical. The example stipulates the bridge and its legal effect to show the typing discipline that an actual cross-recognition instrument would have to supply:
Let LocalChecks_AD(tx_id) and LocalChecks_DI(tx_id) contain the completed local checks. The admitted local packs supply commit_rule_AD and commit_rule_DI, which derive readiness from those checks. Their permits bind the exact rules and transaction context.
adgm_inputs : [ADGM] LocalChecks_AD(tx_id)
difc_inputs : [DIFC] LocalChecks_DI(tx_id)
d_AD : RulePermit(ADGM,LocalChecks_AD(tx_id),CommitReady(tx_id),
code(commit_rule_AD),request_AD) in Delta
d_DI : RulePermit(DIFC,LocalChecks_DI(tx_id),CommitReady(tx_id),
code(commit_rule_DI),request_DI) in Delta
adgm_ready := derive[ADGM,d_AD](commit_rule_AD,adgm_inputs)
difc_ready := derive[DIFC,d_DI](commit_rule_DI,difc_inputs)
MutualRecognition :
CanonBridge(ADGM, DIFC, CommitReady(tx_id)) -- hypotheticalThese carriers record derived readiness, not a new signature on every result. The reusable rule permits support automatic execution.
With the bridge witness, the corridor may coerce one local judgment into the other tribunal:
coerce[ADGM => DIFC](adgm_ready, MutualRecognition)If a local sanctions rule fails or its discretion hole remains unfilled, that side lacks the completed local-check evidence needed for readiness. An absent or inadmissible bridge prevents that recognition use. The commit separately requires both local readiness carriers and the current local action checks. Transporting one side’s evidence cannot replace the other side’s reserved decision.
The executable checker covers the mechanical part of sanctions evaluation through its runtime preflight. The full calculus carries the sanctions effect and terminal constructor. PCAuth fills the two KYC holes. It cannot create MutualRecognition: the hypothetical bilateral instrument must supply that bridge witness through the authority theory. Finite arithmetic and equality checks discharge the reporting-deadline and transaction-identifier conditions. The admission envelope links the filled trace to the compiled payload.
7.8 Temporal Stratification: Statute of Limitations with Tolling
Pakistan’s Limitation Act 1908 s.14 excludes qualifying proceedings prosecuted with due diligence and good faith in a court unable to entertain them for jurisdictional or similar reasons. Explanation I counts both institution and termination days. Article 115 concerns specified contract claims and gives three years, with separate rules for successive or continuing breaches. Section 4 addresses court closure at expiry.3
Qualifying an interval and counting elapsed time are separate operations. A QualifiedExclusion binds claim, proceeding identity, legal ground, endpoints, calendar, authority evidence, and the relevant view. Distinct legal grounds can support the same days. The deadline record retains both grounds and counts their union once.
Fix a calendar c. It supplies ordered time cells, endpoint conversion, month and year addition, and the final court-opening rule. Let N_c(i) convert interval i to its counted cells. For continuous-time half-open intervals, the measure is ordinary length. For the illustrated statutory day convention, an inclusive date interval [a,b] becomes [a,\operatorname{nextDay}(b)). Court-opening adjustment follows the excluded-day calculation and uses its named holiday calendar. It is a separate operation from exclusion.
TollState = (base_deadline, claim, pack, calendar, evidence_map)
Toll(d,e) = d with evidence_map[e.identity] = e
-- identical identity and contents: reuse
-- same identity with different contents: retain conflict
support(d) = union { normalize_calendar(e.interval) : admitted e in d }
deadline(d) = adjust_court_open(base_deadline + measure(support(d)))The same-identity conflict yields an explicit unresolved assessment. It does not replace prior evidence. An authorized correction selects a new assessment view while preserving the history. An unbounded or unresolved interval supplies a provisional bound and pending question, not a fabricated endpoint.
Inclusive dates 1–10 and 6–15 cover 15 distinct days. Both legal grounds remain recorded. The following normalization computes their shared temporal support while preserving their separate evidence.
Normalize a finite interval family by sorting on its left endpoint. Keep the current right endpoint. If the next interval starts before or at that endpoint, replace the endpoint by the larger right endpoint. Otherwise emit the current interval and start a new one. Emit the last interval after the scan. The result is a disjoint union of half-open intervals. Its measure is the sum of their lengths.
Theorem (exclusion conservation). The normalization preserves union, is independent of input order, and is idempotent. Its measure counts each time cell once. Adding duplicate evidence changes neither support nor the derived deadline. The base event and every evidence record remain in history.
Proof. After each scanned interval, the emitted intervals and the current interval have the same union as the processed prefix. Merging an overlap preserves that union. Emitting across a gap keeps the pieces disjoint. Induction proves union preservation and disjointness. The maximal connected components of a finite union are unique, which proves order independence and idempotence. Finite additivity on disjoint pieces gives the measure claim. Evidence-map union and the retained base field give the historical claims. \square
Thus [0,10) and [5,15) contribute 15 continuous units. Inclusive statutory dates 1–10 and 6–15 contribute 15 distinct days. Two grounds covering the same dates retain two legal references and one elapsed-time effect. An admissible new exclusion extends the support monotonically. A correction to qualification creates a distinct assessed deadline instead of rewriting the historical event.
base := derive_1(cause_of_action,selected_pack,claim_period_rule)
d0 := TollState(base,claim,selected_pack,calendar,empty)
d1 := Toll(d0,first_qualified_exclusion)
d2 := Toll(d1,second_qualified_exclusion)
filing_result := filed_by(deadline(d2))This construction supports any finite number of qualified periods. The source events remain Time_0; the assessed deadline remains Time_1. Legal qualification, calendar selection, and any court-opening adjustment carry their own rule and authority evidence.
8. From Calculus to Artifact
The BVI example uses named fields, Boolean conditionals, and a defeasible wrapper. Elaboration resolves that surface program into core syntax while retaining its refinements and effects. Type checking checks the resulting judgment. Evaluation applies the checked rule to entity data.
An implementation begins with a parser for the surface syntax and an elaboration pass producing the judgment G |- s ~> c : A.
The elaborator resolves the prelude, assigns de Bruijn indices, and produces a machine-checked certificate witnessing that every refinement predicate attached to a surface binding survives on the corresponding core term and every surface effect annotation is preserved in the core effect row.
The executable layer requires a bidirectional type checker for the admissible fragment and a runtime evaluator for type-checked rules against entity data. It needs decision procedures for finite-domain membership, threshold comparison, and Boolean propositions.
A proof-obligation extractor walks the AST and emits obligations from its structure: exhaustive match coverage, defeasible-rule guard decidability, and sanctions-check presence. A pretty-printer supplies diagnostic output. A substring-based approximation of the elaboration certificate is unsound: the certificate must be produced by the elaborator as a side effect of the typed translation, not reconstructed from lexical markers on the two representations.
The checker separates bounded execution from total logical decision. First, a fuel-bounded checker attempts pure reduction and structural comparison for source definitional equality. It must use \to_c, and its treatment of substitution must respect the declared size bound. Completeness requires the open weak-head and conversion theorems. Exhaustion is an operational result, not a proof of inequality or non-compliance. Second, a total decision interface returns a proved alternative under the conditions of Section 4.2. Evidence acquisition and general search may instead return Await, Unknown, or a typed error. Their handlers preserve the pending query and supplied evidence. Termination of a fuel-bounded handler establishes a result of that handler. It does not establish completeness of the underlying search.
A tabular authoring surface, decision tables compiled to canonical Lex AST, captures the rule patterns practitioners most often write (a rule name, a jurisdiction, a legal basis, and a set of condition-verdict rows with priorities). The tabular surface compiles directly to the defeasible lambda match pattern without extending the core AST. It is an accommodation to authoring practice.
The tabular lowering carries the same meaning-preservation burden as the elaboration pass. Four obligations attach: each condition form lowers to a match whose taken branch is equivalent to the condition’s satisfaction in every runtime context; a row’s conditions conjoin, so the row’s outcome fires only when all hold and evaluation otherwise falls through; the compiled cascade agrees with the table’s first-row-wins reading and reduces to the mandatory default when no row fires; and the compiled defeasible rule agrees with the source table’s evaluator on every well-formed input. This is translation validation in the sense of Pnueli, Siegel, and Singerman (1998). The obligations are recorded per rewrite rather than mechanized, and, as with the elaboration certificate, agreement on a suite of sample tables does not discharge them.
An external SMT backend, using the SMT-LIB2 exchange format, can search for answers beyond the fragment’s built-in decision procedures. Discharging an obligation requires either a checked proof certificate or an explicitly admitted trusted-solver premise recorded with that obligation. A solver response alone is not a proof term. Unavailable solvers, timeouts, and unsupported problems return Unknown; they supply no verdict.
Section 5.1 states the schema for compilation of the admissible fragment into Op bytecode. The open reference model (Lorgat 2026g) closes nine finite preservation cases; compiler coverage, completeness modulo operational outcomes, and full abstraction remain open.
A certificate that verifies only the separate hashes of statute text and rule text proves no relation between them. The counterexample is Singapore Companies Act 1967 s.171: a secretary-presence rule can preserve both hashes while omitting the six-month appointment period, ordinary-residence requirement, and sole-director prohibition.
A statute has no evaluation semantics, so “the rule equals the statute” is not a formal statement. One can instead compare Lex with an independently authored decision table or reference trace over an enumerated input set. The joint-trace digest witnesses that comparison. Agreement bounds divergence between two formalizations; it does not prove identity with the statute.
A fidelity claim therefore carries a deficit register. Each entry names an undecided clause, its reference, and the reason. An empty register claims full coverage. Because the register is authored, its completeness is an attestation rather than a derivation.
9. Conditional Semantics
The typing rules specify valid expressions. A semantic model must assign meanings to them and explain why substitution and reduction preserve those meanings. Section 7.2 supplies the first requirement: changing the jurisdiction must also change the permitted entity data.
A category records objects and composable maps between them. A category with families (CwF), in Dybjer’s sense, adds types and terms over each context. Context extension represents adding a typed variable. Reindexing interprets substitution. A full split comprehension category with chosen stable dependent sums and products presents the same structure needed here; no equivalence with arbitrary comprehension categories is claimed. Contexts are objects, types are dependent families over contexts, and values are sections of display maps. Computations use the indexed outcomes of Section 4.2. The semantics are conditional on the bridge and adequacy obligations below; mechanization of the full-calculus semantics is open.
A display map forgets the newly added variable from an extended context. A section supplies a value for that variable at each context. Dependent sums package a value with dependent evidence. Dependent products describe functions that supply such evidence for every input. The adjoints below express their introduction and elimination laws.
A categorical model of Lex consists of:
A CwF
(Ctx, Ty, Tm, 1, .)with comprehension objectsΓ.A, display mapsp_A : Γ.A -> Γ, and generic terms.A comprehension-category structure in which reindexing along each display map has left adjoint
Σ_Aand right adjointΠ_A, so dependent sums and products are interpreted as adjoints.Universe objects interpreting
Type_l, closed underΠandΣ, with cumulativity.A proposition subfibration
Prop(Γ) ⊆ Ty_0(Γ)whose fibers are Heyting algebras.For each tribunal
T, a dependent family of runtime evidence carriers. At environmentgamma, its elements are pairs(v,p)wherevinhabits the interpreted interface andpis a finite certificate accepted by the checker of Section 4.6. Direct evidence contains an Issued node. Derived evidence contains its source acts and checked rule receipts. Reindexing acts on typed references and their indices, preserving each opaque closed act record. A changed immutable request needs evidence at the new index.A temporal index category [1] = (0 \to 1): the two-object category with one non-identity arrow 0 \to 1 and no reverse arrow.
Time_0lives over0,Time_1over1, andlift_0along the arrow; the missing arrow 1 \to 0 is temporal non-regression stated at the index level. The asymmetry is deliberate: a group-graded index would supply an inverse and readmit the Time_1 \to Time_0 move that the typing invariant forbids.
The judgment interpretation is:
⟦Γ⟧is an object of the CwF.⟦Γ ⊢ A : Type_l⟧is an element ofTy_l(⟦Γ⟧).⟦Γ ⊢v v : A⟧is an element ofTm(⟦Γ⟧, ⟦A⟧).⟦Γ, x : A⟧ = ⟦Γ⟧.⟦A⟧.A dependent product of values, written \Pi_v(x:A).B, denotes \Pi_{\llbracket A\rrbracket}\llbracket B\rrbracket. A function with a computational body has value interpretation \llbracket\Pi(x:A)[\rho].B\rrbracket_\gamma =\prod_{a\in\llbracket A\rrbracket_\gamma} \operatorname{Comp}_\rho(\llbracket B\rrbracket_{\gamma,a}). Constructing this function value performs no body effects. Calling it selects the computation at the supplied value. An empty effect row alone establishes neither termination nor a returned value. Dependent sums retain their value interpretation:
⟦Sigma(x : A). B⟧ = Σ_⟦A⟧(⟦B⟧).\operatorname{Evidence}_{T,A,\gamma} =\{(v,p)\mid v\in\operatorname{Value}_{A,\gamma}, \operatorname{CheckCert}_{\Delta}(T,A,v,p)=\mathrm{true}\}. The checker uses the actual typed program and recorded transition evidence at Computed nodes. It retains exact issuance and use indices.
The temporal sorts are the two fibers of the graded temporal presheaf defined below. Their only cross-grade map is \texttt{lift\_0} : \texttt{Time\_0} \to \texttt{Time\_1}.
In Section 7.5, the evaluator knows the answer type before receiving the answer. Its semantic object must retain the request and continuation. An admitted fill supplies a value in that response family and permits the continuation to resume.
Computation families require reindexing of their request signatures, response fibers, continuations, and effects. These maps must commute with return and bind while preserving admitted authority and value indices. The set-family construction supplies these operations at a fixed signature. The full authority-indexed presheaf interpretation requires their naturality and universe closure separately.
Pure substitution is reindexing in the CwF. Its value-level equations are equalities of sections. Effectful evaluation uses computations over these families and preserves its observable execution prefix.
Recognition can refuse or request further evidence even when a source value exists. Its target must retain computation outcomes. Two routes can return the same verdict while disclosing different records or leaving different duties. Those routes remain observably different under the interpretation below.
Bridges act on computations. Let V_{T,A,\gamma} denote accepted values at tribunal T, interface A, and context \gamma. A CanonBridge(T,U,A) interpreter preserves interface A. A route to a different interface B first recognizes that evidence at U, then applies a separately admitted local rule from A to B. The composite route has type b_\gamma:V_{T,A,\gamma}\longrightarrow \operatorname{Comp}\bigl(V_{U,B,\gamma}\bigr). Writing r_\gamma:V_{T,A,\gamma}\to \operatorname{Comp}(V_{U,A,\gamma}) for recognition and f_\gamma:V_{U,A,\gamma}\to\operatorname{Comp}(V_{U,B,\gamma}) for the admitted local rule, b_\gamma(v)= \operatorname{bind}(r_\gamma(v),f_\gamma). A bridge alone is the case B=A with the identity local continuation. At source level, the composite is derive[U,d](f,coerce[b](m)), where d : RulePermit(U,A,B,code(f),r) is admitted separately from the bridge witness. Its effect budget includes both stages’ rows and authority(U). The existing coerce, derive, and bind constructors retain the recognition and local-rule certificates. This decomposition matches Tribunal-Coerce and RulePermit in Section 4.6. The request signature retains its authority, source, scope, and response fiber. The interpreter can return an accepted value, refuse, emit an effect, or suspend for a typed response. If the target fiber is empty, a refusal still inhabits the computation space. A singleton source fiber therefore poses no contradiction.
Composition is (c\star b)(v)=\operatorname{bind}(b(v),c). It carries every intermediate effect and unfulfilled duty into the next stage. Disclosure events remain in the recorded prefix. A route comparison must preserve returned values, refusal evidence, outstanding requests, authorized effects, duties, and disclosures. Associativity reassociates sequencing while preserving this observation. Identifying routes only by their final verdict would discard part of the result.
Pure context reindexing has a different type. The base category below contains declared total value transports, written \operatorname{PureTransport}(T,U,A). Such transports preserve accepted value fibers and perform no effects. Each has identity and composition laws. Effectful CanonBridge interpreters retain the computation type above. Establishing a natural family of these interpreters at the same interface requires its own context and authority compatibility proof. Routes changing interface also require that proof for the local-rule stage.
A presheaf assigns a set of values to each context and a compatible map to each change of context. Compatibility means that identity and successive context changes act consistently. This model can retain the authority and temporal stratum of a value. The smallness premise below supports the standard dependent-type constructions.
The concrete model lives inside a presheaf topos. For each fixed interface A, let AT_A be the category of authority-contexts, under the smallness hypothesis that the deployed authority labels, total value transports, and temporal strata are drawn from a fixed small universe. The transport identities and composition laws hold in that universe. This hypothesis is structural: AT_A^op -> Set is a presheaf topos only when AT_A is a small category. A multi-interface context is interpreted by a fibration of these categories over interfaces; the single-category notation below suppresses that index only inside one fixed interface.
Objects are pairs
(auth, t)whereauthis a tribunal or authority label andt ∈ {0,1}is a temporal stratum.Morphisms are oriented opposite to object-language transport so that presheaf reindexing has the Lex direction: \operatorname{Hom}_{AT_A}((T',t'),(T,t)) :=\operatorname{PureTransport}(T,T',A)\times \operatorname{Hom}_{[1]}(t,t'), where
Hom_[1](0,0),Hom_[1](1,1), andHom_[1](0,1)are singleton sets andHom_[1](1,0)is empty. Thus a pure value transport b:\operatorname{PureTransport}(T1,T2,A) appears as a base morphism(T2,t) -> (T1,t), and the presheaf action along that morphism is a map⟦[T1]A⟧ -> ⟦[T2]A⟧, interpreting total value transport. General bridge coercion uses the computation interpretation above.Composition is componentwise in the reversed base orientation: the value-transport component composes its total maps, while the presheaf arrow points in the opposite direction.
The identity and associativity laws for AT_A are the specified laws of total value transport. For this small category, the presheaf category AT_A^op -> Set is a topos and therefore locally cartesian closed (Seely 1984). It carries the canonical presheaf CwF: contexts are presheaves E, types over E are display maps p : A -> E, and terms are sections s : E -> A. Reindexing is pullback, while Π and Σ are the right and left adjoints to pullback along display maps. In particular, every closed value type at interface A is interpreted as a presheaf AT_A^op -> Set, and every open type is a dependent presheaf over the presheaf interpreting its context.
Let D be the set of dates and C the set of derived-time closures. The graded temporal presheaf Time has fiber D at stratum 0 and fiber C at stratum 1. The base arrow (auth,1) -> (auth,0) induces the restriction map D -> C given by lift_0. There is no base arrow in the other direction, because Hom_[1](1,0) is empty, and hence no restriction map from derived time to frozen time. This is one presheaf with two graded fibers, not two unrelated set-valued interpretations.
For the accounts example, an accounting event supplies a frozen date. The selected pack and admitted notice determine its derived deadline. A revised assessment produces another derived record while retaining that event. This is the role of the two temporal fibers above.
Base data types are constant presheaves. Compliance verdicts are interpreted in the constant presheaf ΔH_verdict, where H_verdict = {NonCompliant < Pending < NotApplicable < Exempt < Compliant} is the five-element Heyting chain of §7.4. Its constant structure maps define an internal algebra. In particular, ΔH_verdict carries internal Heyting-algebra structure: the structure maps ∧, ∨, ⇒ : (ΔH_verdict)² → ΔH_verdict are presheaf morphisms by naturality, since they are constant on objects and hence commute automatically with every reindexing functor along a morphism of AT. Meet, join, and the relative pseudocomplement of §7.4 transport to the presheaf model pointwise.
The verdict NonCompliant is an inhabited value at the bottom of the verdict chain. The empty value type 0 is interpreted by the empty presheaf. Sanctions dominance instead denotes a refusal in F_\rho 0, retaining the admitted violation evidence. A nonempty context can have a section of that computation family. It supplies no section of the empty value family. Section 4.12’s Abort-Map therefore preserves refusal while changing the declared return type.
Here D denotes the compliance-domain set of Section 7.4, and D' is its fixed evaluated support. The preceding temporal example used D locally for dates.
The scalar projection of the Lex verdict layer is the product presheaf (\Delta H_{\mathrm{verdict}})^{D'} for a fixed finite support D'\subseteq D, with meet and implication componentwise. The pointwise Heyting laws hold within each fixed-support fiber. The full product over D applies only when coverage is complete. Missing fibers remain coverage data, as in Section 7.4; they acquire no default verdict. It is not the full compliance-state model of How Compliance Composes, which separates compliance grade from applicability. TensorAlignment.v proves that lex_to_tensor : ΔH_verdict → V_tensor is injective and preserves meet on Applicable values. PropagationAlignment.v proves that verdict_to_cs and cs_to_verdict are inverse maps preserving rank, meet, and order. These are explicit transport results, not an isomorphism with the mixed-axis compliance state.
Three objects have separate roles: the scalar verdict, a proposition asserting a property, and the certificate accepted by an authority. A Compliant scalar supplies neither every required proof nor the certificate needed for execution.
The proposition fragment is interpreted by subobjects in the presheaf topos. Its Boolean fragment consists of complemented subobjects with explicit decision sections. The classical rule is derived from those sections. General temporal subobjects retain Heyting implication and negation. This truth algebra differs from the constant verdict algebra. Runtime tribunal evidence remains a certificate carrier. For A:Prop, [T]A contains the evidence needed for execution, while ||[T]A|| expresses logical inhabitation. The latter cannot reconstruct a certificate or an issued act.
The carrier above has a concrete interpretation: finite accepted certificate graphs paired with their exact values. Assert selects an admitted Issued node. Derive checks a typed rule trace and constructs Computed evidence. Open joins dependencies through Cut. Coerce preserves the original acts and records destination recognition. There is no unconditional unit from arbitrary A to [T]A. An authenticated reusable rule can authorize a particular computation without authorizing every proposition or caller.
The implementation proof must establish that the certificate checker accepts exactly the stated constructors under their binding conditions. The substitution proof must preserve the exact value, request, program, and context indices. Existing bridge-function laws apply to their extensional target. Their lift to these certificate carriers must retain provenance, destination decisions, and current-use boundaries. These are concrete adequacy lemmas for the specified construction.
The presheaf construction supplies candidate meanings for values. Adequacy must connect these meanings to source typing and reduction. Computation adequacy must also preserve refusals, requests, and the execution prefix. The next obligation separates these tasks.
Open obligation (adequacy of the current pure admissible fragment). If Γ ⊢ e : A is derivable in the current L_adm fragment, then for every object c of AT and every environment γ ∈ ⟦Γ⟧(c), the denotation ⟦e⟧_c(γ) is defined and belongs to ⟦A⟧_c(γ). Moreover, if e\to_L e' within the declared pure fragment, then ⟦e⟧ = ⟦e’⟧; hence if e ⇓ v, then ⟦e⟧ = ⟦v⟧. This obligation ranges over the pure value fragment. An effectful term instead denotes a computation whose return branch inhabits the declared value family. Refusals and requests remain typed outcomes with their execution prefixes. Their adequacy theorem must relate all four outcome constructors.
Required proof, by constructor. Induct on the typing derivation. The current L_adm scope covers the standard CwF cases admitted by the fragment, finite constructor matches, defeasibility, and effect-row cases. The full calculus creates a second obligation: dependent pairs where admitted, tribunal modals, temporal stratification beyond pointwise proposition formers, and discretion holes. The case table below records those cases as semantic obligations, not as parts of current L_adm.
The case table below fixes, for each constructor class, its interpretation and the obligation a full closure must discharge beyond a standard CwF.
| Case | Interpretation | Obligation beyond a standard CwF |
|---|---|---|
| Value variable, sort, Pi, lambda, pure application and let | Standard CwF clauses (Dybjer 1996, §3; Jacobs 1999, ch. 10); universes per Hofmann-Streicher (1998), cumulativity as upward inclusion | Structural source regularity, typed substitution, pure product compatibility, and the specified source trace preservation are closed. Source-to-CwF conversion and computation refinement remain required |
| Match | Pointwise finite case analysis on the scrutinee, with branch contexts reindexed along the constructor-extended display map | Well-definedness rests on the admissible fragment’s finite-variant restriction on match |
| Defeat | Pointwise priority-ordered scan: the highest-priority firing exception’s body, else the base body | Naturality of each guard and body under context reindexing, with preservation of their observed effects |
| Tribunal modals | Values paired with accepted Issued, Computed, Recognized, and Cut certificate graphs; coercion retains source acts | Certificate-checker adequacy, indexed substitution, provenance preservation, and the certificate-level lift of bridge action |
| Temporal stratification | Fibers over the temporal index category [1]; lift_0 rides the arrow 0 \to 1; reevaluate lifts pack replay within the fiber over 1 |
Non-regression transports to the model because [1] has no arrow 1 \to 0; standard CwFs do not stratify their universe by an asymmetric index |
| Typed discretion holes | A request carries its exact response family and continuation. An admitted response supplies a value in that fiber | Authentication, current-use checks and continuation preservation must refine the request transition |
| Effect rows | A computation grade bounds its observed effects. Effect-Weaken includes a smaller grade in a larger one | Trace soundness and union must commute with pure context reindexing |
Preservation of denotation under pure reduction (the second clause of the obligation) requires induction on \to_L restricted to that declared pure fragment, using the CwF beta/zeta/iota equalities for the standard cases and the per-case denotational equations spelled out above for the Lex-specific cases.
Mechanization of the full presheaf adequacy theorem remains open beyond the flat fragment; each Lex-specific row of the case table is a separate proof obligation. The Mechanization Boundaries table at the end of §5.1 classifies adequacy as open.
Full abstraction. Full abstraction for the complete Lex calculus remains open. The certificate carrier retains distinctions between source acts, rule receipts, bridge paths, and evidence views. A projection to payload values forgets those distinctions and is not fully abstract for an observer allowed to inspect the evidence bundle. The full abstraction theorem must compare the actual runtime’s observable outcomes, authority uses, suspensions, and provenance with those of the certificate-sensitive model. Set-valued carriers can retain certificates; a payload-only interpretation chooses to omit them.
A cut first constructs an intermediate result and then consumes it. Cut elimination removes that detour while preserving the final judgment. The modal extension considered below is broader than the current admissibility predicate. Section 12 separately states the obligation to admit those modal forms.
Conjecture (principal-cut normalization). Fix a fragment, context \Gamma, and program-reduction relation. Assume subject reduction in that fragment and strong normalization under \Gamma. Every enabled principal-cut contraction must preserve the context, result type, and fragment membership and induce a nonempty step under that same relation. Administrative contractions inducing no term step must decrease a separate well-founded measure. Under these premises, repeated contraction reaches a derivation with no enabled principal program cut, preserving its context and result type.
Proof strategy under the stated premises. A principal program cut composes an introduction with its consuming elimination: beta for Pi, zeta for let, iota for a constructor-headed finite match, and the finite dispatch redex for defeasible selection. Subject reduction preserves each successive judgment. Strong normalization rules out infinitely many simulated nonempty term steps, and the additional measure rules out an infinite administrative tail. Repeated enabled contraction therefore terminates. This gives principal normality. Neutral eliminations and suspended authority requests need not contain an enabled principal redex.
The closed-term SN-admissible conjecture of Section 5 does not supply normalization in an arbitrary open context. An open-context theorem or a proved closure argument is required. The flat affine result in FlatAdmissibleSN.v supplies its stated closed normalization case. Extending the construction to dependent matches or tribunal modals requires an enlarged admissibility predicate and preservation and normalization for that same enlarged fragment. The additional modal contractions include tribunal-open, tribunal-coerce-id, and tribunal-coerce-comp; their simulation must retain authority evidence, outcome, and execution trace. Reaching Await does not establish cut-freeness.
Full derivational cut elimination remains open. Its intended conclusion is a cut-free derivation with the same context and result type. To establish it, the paper needs an explicit derivational Cut syntax, principal and commuting conversions including neutral eliminations, preservation, and a total coverage theorem saying that every remaining derivational cut admits a valid contraction. Those contractions must satisfy the simulation and termination premises above. Without coverage, absence of an enabled principal redex does not imply absence of every derivational cut. Confluence is not needed for the conditional termination argument.
The Cut(m,n) nodes of Section 4.6 are retained provenance certificates. They record how evidence was used and may remain inside a returned value after program reduction. They are not the derivational cuts targeted by this open theorem. Neither program normalization nor derivational cut elimination may erase issued-act identities or the evidence references required by the observer.
11. Scope of the Contribution
The core calculus makes these distinctions syntactic. Finite mechanized fragments establish temporal non-regression, re-evaluation source preservation, receipt locality, priority evaluation, and quorum extraction. The structural source core has closed weakening, typed substitution, and regularity theorems. Pure source conversion is confluent, and the fourteen-rule reduction relation preserves assigned types along finite traces in generated well-formed contexts. Full operational preservation, unconditional progress, symbolic execution confluence, strong normalization for the full admissible fragment, and proof-relevant adequacy remain open. A proved sanctions violation blocks in the full calculus. Executable preflight requires a refinement proof to the same proof-bearing refusal and suspension contract.
The examples determine the scope of the results below. A source typing theorem concerns expressions. A model theorem concerns its chosen mathematical carrier. An implementation theorem must relate that carrier to actual execution. The list retains those separate claims.
Contributions.
Tribunal evidence separates exact issued acts from results computed under reusable rule permits. Its bridge interpreter preserves source acts, destination decisions, intermediate effects, and suspension. The abstract function-bridge model is closed. Actual-syntax, certificate, and runtime adequacy proofs remain open.
Defeasibility separates priority from control flow: rules order on a priority graph and evaluate in a Heyting verdict lattice. Overrides and residual obligations are explicit.
Typed discretion holes carry value-indexed PCAuth witnesses with multi-signer quorum, revocation metadata, linked timestamp anchoring, and bounded delegation. A filled hole records who signed, under what authority, in what scope, and against what temporal conditions; the structural quorum-extraction theorem is closed in Rocq.
Temporal stratification is first-class through
EffectiveDate,Repeal, stackedToll, and pointwise admissibility-time temporal proposition formers. Statutory change is typed structure; temporal non-regression and re-evaluation source preservation are closed over the object-language grade and pack-witness cores.The flat admissible fragment is a strongly normalizing calculus of proof terms for finite compliance propositions. Extending that reading to holes, tribunals, and time remains open.
Conditional categorical semantics in a category with families and a presheaf model over bridge contexts, with strictification, bridge-action naturality, adequacy, and full abstraction left as explicit obligations.
A closed receipt algebra for admission hosts: composing Lex receipts by verdict meet and obligation/frontier union is associative, has the expected greatest-lower-bound property on verdicts, and satisfies receipt locality (
accepted/compliantcompose iff each component does).The closed equations concern the projected receipt carrier. Legal and operational admission retain Section 7.4’s additional premises.
A decidable syntactic admissibility predicate. Decidable type checking, preservation, unconditional progress, confluence, and strong normalization for the full admissible fragment remain open (Mechanization Boundaries, end of §5.1).
The implementation repository is https://github.com/momentum-sez/lex. Its availability alone does not identify the complete proof snapshot. The accompanying supplement, supplements/lex-proof-supplement.zip, is located relative to this PDF. It fixes the source snapshot for the bounded source conversion and trace results. Its SHA-256 digest is df50da81307605f254cc9007b96ff587fcfc29270dcea97bbd61fe34fd7d1ffe.
The supplement contains ProductCompatibility.v, BetaPreservation.v, BetaTracePreservation.v, and Examples.v, with their dependency sources. It supplies exact source hashes, source-to-object bindings, pinned compiler identities, library manifests, reproduction instructions, commands, and build logs. The recorded build of 5 September 2026 (UTC) compiled all 25 unchanged proof modules from a fresh extraction. It used Rocq 9.1.1, compiled with OCaml 5.4.1. The recorded checks comprise two successful kernel checks, 119 original assumption reports, and 21 named exported reports. Each assumption report is closed under the global context. The installed library recipe identifies Stdlib 9.0.0. Complete library manifests identify the exact installed bytes.
These records concern the fourteen-constructor source subrelation. They retain the exclusion of 42 operational constructors. The supplement supplies a consolidated record for this fresh build. The historical final receipt remains absent. These records do not establish historical compiler and object binding retroactively. Exact historical-object and cross-platform reproduction remain unestablished. Rebuilding requires the pinned installed toolchain; its installation requirements and identity checks accompany the source. Compiler binaries are not bundled.
The relative download and digest identify the accompanying supplement. A persistent public archive with an immutable identifier remains an additional requirement for archival reproduction. Full-language soundness and compiler/runtime correspondence remain open. A statement called closed has a Qed proof and no admitted lemma; every classical or extensionality dependency is named. The mechanization table in §5.1 identifies each statement’s source module and exact formal status.
The contribution is a logic in which precedence, legal time, asserting authority, and typed discretion are primitive. Its finite cores close temporal rule-graph non-regression, pack source preservation, quorum extraction, receipt locality, a fail-closed admission envelope, a finite event-union lemma, and a strict function-bridge target. Strong normalization is closed for the flat admissible fragment. The structural source core has weakening and dependent substitution. Every type assigned there has a universe in a generated well-formed context. This result uses formed conversion targets and the pure conversion relation. Pure conversion has a common-reduct theorem and exact product compatibility. The specified fourteen-rule relation additionally preserves assigned types along finite source traces. Full-fragment checking still requires full operational preservation, symbolic confluence, progress, and normalization.
Each operational theorem applies to its stated fragment and primitive contracts. The full calculus carries the wider syntax and conditional semantics. Section 12 states the exact obligations between them.
Two further limits remain. First, the paper is about semantic and metatheoretic structure, not an empirical study of large rule corpora. Second, the comparison with Catala, L4, and related systems is argued at the level of constructs and examples rather than proved by a formal translation theorem.
12. Open Problems
The remaining work must connect the constructed parts without losing their indices or evidence. The first obligations concern typing and execution. Later questions concern external authority, rule evolution, and compilation. Each requires the assumptions named in its statement.
Full metatheory of the modal and dependent fragment. Administrative head reduction is bounded. Checking for the current admissible fragment still requires preservation, unconditional progress, confluence, and its complete weak-head and normalization results. An extension admitting dependent matches, tribunal transport, temporal operators, and delegated hole fillings requires a newly specified admissibility predicate and those results for its own enlarged syntax and aligned reduction relations. The current Section 5 predicate is unchanged. The cut-elimination goal in Section 9 additionally requires derivational cut syntax, commuting conversions, and coverage; principal program normality is insufficient. For the wider symbolic relation, Confluence.v proves that the parallel-star diamond implies confluence. Its diamond property remains open. This is separate from the closed pure source confluence theorem in ProductCompatibility.v. Progress retains its confluence and finite match-coverage premises. Full operational preservation and full-fragment normalization remain open.
These obligations have a mathematical dependency order. Source substitution and regularity are closed. The separate pure parallel development supplies its substitution, triangle, and embedding lemmas, proving pure source confluence and product compatibility. General beta preservation follows, and BetaTracePreservation.v closes finite traces through its seven head rules and seven recursive contexts.
Preservation remains open for application arguments, constructor firing, the omitted binder and type fields, and the wider execution forms. These cases require the corresponding formation, signature, substitution, and effect-typing arguments. The symbolic parallel relation retains its own substitution, shifting, and diamond obligations. Constructor signatures and finite coverage must support match preservation and progress. Full normalization must extend the flat result to dependent functions, matches, effect rows, and filled-hole evidence. The modal and temporal interpretations retain their own formation and adequacy clauses.
Fully constructive mechanization. One priority-graph acyclicity lemma uses classical description, and two propagation-graph lemmas use functional extensionality. The recursive syntax itself has closed mutual equality procedures. Constructive graph search can replace the classical acyclicity step. The remaining categorical and operational statements are classified in the Mechanization Boundaries table.
Revocation dissemination across corridors. A typed revocation Revoke(cred) invalidates a verdict filled at or after revocation and taints one filled earlier. The open problem is the dissemination condition under which independently verifying jurisdictions converge on the same tag.
Revocation and pack-relative re-evaluation. Lex now records quorum, delegation, and timestamp structure inside PCAuth, but it still needs a complete semantic policy for what happens when a delegated authority is revoked, expires, or is later overruled after a hole has been filled. The open question is how those revocations interact with repeal, tolling, and rule-pack migration without corrupting the frozen historical record.
Priority against repeal. Priority graphs and temporal operators are now both first-class. What remains open is a jurisdiction-indexed doctrine for cases in which a later repeal or superseding enactment conflicts with an earlier but more specific rule. The language can represent both axes; the legal resolution policy is not uniform across jurisdictions and is not fixed here.
Pack-indexed admissibility. Pack objects, rewrite witnesses, and repeal terms are now typed in the core calculus. What remains open is integrating pack selection into the admissibility predicate. For the admissible fragment, the checker must show that only a finite pack history is relevant to any evaluation and that proofs of Active(r, P, t) do not introduce cycles through rewrite search.
Pack-evolution soundness for the modal and temporal subsystem. Section 3.3 defines typed packs, replay-carrying rewrite witnesses, and a closed re-evaluation step for derived-time closures. What remains open is the full proof that the same construction commutes with arbitrary temporal terms, temporal modals, tribunal modals, and the admissibility predicate once pack indices are internalized into Time_{1,P}. This is stated there as a conjecture.
Semantics of nested discretion holes. Value-indexed sequencing in Section 4.2 orders fillings that depend on earlier returned values. The general problem is to compile arbitrary hole dependencies, detect cycles, and retain exact request indices through suspension.
Compilation to ZK circuits. A zero-knowledge proof that a compliance evaluation was performed correctly, without revealing entity data, would enable privacy-preserving regulatory reporting. The open obligation is to define a compiler from typed Lex evaluation traces to rank-one constraint systems (R1CS) or PlonK-style arithmetic circuit relations, and prove circuit soundness preserving verdicts, types, obligation frontiers, and PCAuth bindings. This target is conditional on the source metatheory and WHNF-bound closure above; before those close, a circuit proves only the bounded trace relation it encodes. Groth16 and PLONK are natural candidate proof systems, but the paper does not claim a closed compiler.
Full modals in the admissible fragment. The current admissible fragment rejects all modal forms (temporal, tribunal). Extending admissibility to include modals while preserving decidability requires a stratification argument: modal operators must preserve acyclicity in the dependency structure. The temporal stratification check enforces the necessary invariant (Time_1 cannot coerce to Time_0) locally. Integration with the admissibility predicate remains open.
Oracle termination as an authority claim. When a rule invokes an external oracle, the obligation terminates_by oracle O: depth <= k is discharged at the proof-checking boundary by a signed attestation from the oracle operator together with a runtime bound check: the evaluator aborts the oracle at depth k and records whether the oracle produced an answer before the bound. This is an authority-backed trust assumption (the operator signs a termination claim) plus runtime enforcement by the counter. A mechanized termination proof for a specific oracle class, for example ownership-chain traversal bounded by graph diameter, would replace the signed claim with a checked derivation.
Type inference. The bidirectional discipline requires type annotations on lambdas (checking mode) and explicit annotations on terms that cannot be inferred. A unification-based inference algorithm for the admissible fragment would reduce annotation burden, but unification in the presence of defeasible rules and effect rows is nonstandard.
Privacy-preserving proof transport. The admissible fragment remains a plausible source for privacy-preserving regulatory reporting, but a sound compilation of Lex derivation traces to succinct proof systems remains open. The open question is how to preserve the language’s typing guarantees under circuit or proof-system compilation.
Deficit-register completeness and automated deficit detection. The deficit register of Section 8 is authored. Deciding, from the statute text and the rule, whether the enumerated register is complete is open; any automation crosses the same natural-language boundary the authored reference semantics was introduced to manage. Partial targets — clause-level alignment against structured statute markup (Section 10.5), quantifier and threshold extraction — are research directions, not claims.
The remaining questions are stated with their exact mathematical boundary.
12.1 Bounded Legal First-Order Quantification
Jurisdictional rules routinely quantify over bounded domains: “every beneficial owner with a stake above 25 percent,” “all parent entities in the ownership graph,” “some authorized director in the resolution set.” Section 4.2 introduces the bounded quantifiers forall x : A in C. P(x), exists x : A in C. P(x), and exists! x : A in C. P(x) ranging over Collection(A) with a finite enumeration, together with witness extraction choose; the effective finite decision proposition and constructive finite choice proposition at the end of §4.2 give the expansion into and_fold, or_fold, and finite uniqueness checks, along with the bounded-search discipline for choose. Two questions remain open. First, which statute-derived predicate shapes admit decidable quantifier elimination? Linear arithmetic over enumerated bounded domains admits Presburger procedures (Bradley and Manna, 2007), but no uniform treatment across jurisdictions or with the tribunal-modal and temporal strata of §§4.5-4.6 is proved here. Second, do the temporal sorts of §3.2 and authority indices pass through bounded quantifiers without loss of information? The admissibility argument proves this pointwise, but not uniformly. The higher-order meta-quantifier Pi_meta (§4.2) remains outside the admissible fragment. Admitting it would require reflection over rule syntax and metadata rather than bounded iteration; that is a separate open problem.
12.2 Curry-Howard Correspondence
The Curry–Howard correspondence reads propositions as types and proofs as their inhabitants. For Lex, that reading must preserve the authority and time conditions carried by a judgment.
The open Curry-Howard theorem must identify the Prop fragment with a constructive type theory and read a valid hole fill as a proof of phi_h(v) ∧ authorized(h, signer) ∧ temporally_admissible(audit) whose scope projection is ScopeWitness(h.scope,v).
12.3 Logical Relations and Parametricity
A polymorphic rule should use an abstract input through its declared interface. Parametricity states the resulting uniformity: related inputs produce related outputs. Lex must specify those relations for time and authority as well as ordinary values.
The open abstraction theorem is parametricity for prelude-polymorphic types, with temporal grades and equal authority scopes as the two principal relations (Reynolds 1983; Wadler 1989; Bernardy, Jansson, and Paterson 2010).
12.4 Prop-Sort Discipline and Proof Irrelevance
Erasure must remove proof-only terms while retaining certificate fields that execution and later review inspect. Consistency must establish that the proposition rules cannot derive falsity without such a premise.
The open result is consistency and certificate-preserving erasure for the exact Prop rule set of §4.1, including Subset, Squash, J, certified Boolean calculation, and non-empty effect rows.
12.5 Higher-Dimensional Equality and HoTT/Cubical Treatment
The current identity rules already support equality reasoning. Higher-dimensional equality would add relationships between equality proofs themselves. Such an extension needs its own justification for the evidence operations used here.
Homotopy type theory (HoTT) studies types through their equality structure. Lex uses intensional identity and J; adding cubical paths or univalence requires a separate consistency and certificate-composition theorem and is not assumed here.
12.6 Modal Soundness and Completeness for Tribunal Bridges
The open modal theorem is soundness and completeness for a Kripke semantics whose accessibility relation is witnessed by tribunal bridges (Pfenning and Davies 2001; Nanevski, Pfenning, and Pientka 2008).
Recognition can also refuse or suspend, as Section 9 describes. The proposed semantics must retain those outcomes. An accessibility relation alone supplies no accepted destination value.
12.7 Denotational Semantics and Full Abstraction
Adequacy and full abstraction require preservation of PCAuth witnesses, bridge witnesses, execution outcomes, and derivation traces. Set-valued models can retain them as data. The open task is to prove agreement between source and target observations.
12.8 Full-Fragment Metatheory Beyond the Admissible Core
The full language with recursion, higher-order witnesses, and unbounded audit chains needs fixed-point semantics plus progress modulo divergence; those claims are separate from the finite admissible fragment.
12.9 Discretion-Hole Lifecycle Beyond Hart’s Penumbra
The dynamic semantics of a discretion fill remains open: acknowledgment, challenge, affirmance, and appellate retraction must preserve its authority, scope, and temporal indices.
12.10 LTL/CTL/TCTL over Execution Traces
Lex’s two temporal sorts do not express behavioral temporal logic. LTL/CTL/TCTL properties of Op traces, including eventual hole resolution and revocation safety, require a separate source-to-trace theorem.
12.12 Governance of Wire-Schema Evolution
The Lex repository is licensed under Apache-2.0. The license permits reading, modification, and redistribution. It does not allocate control of canonical encodings. Every typed object that crosses a system boundary has a wire schema: the pack and its content-addressed digest (§3.3), the PCAuth witness and its canonical signed payload (§3.5), the bulletin stamp (§4.10), and the receipt consumed by an admission host (§7.4). A conforming implementation accepts exactly those encodings. Control of an encoding therefore determines which values implementations accept, which digests remain stable, and which signatures verify. Standards-body governance would require a published amendment procedure, versioned schemas with a compatibility rule, and a forum whose membership extends beyond one implementation’s authors. This paper defines the schemas and their digests. It does not create that forum. Until such a forum exists, Lex is open as source code, not as a governed standard.
Accession Networks (Lorgat 2026e) defines the standards body’s governance and accession instrument. Lex defines the schema those rules carry.
13. Conclusion
Lex records authority, defeasibility, legal time, and authorized human judgment in the types and evidence of a compliance program. Its formal constructions give those requirements explicit roles: tribunal modals are interpreted over explicit bridge data; defeasibility is separated from control flow by priority graphs and a Heyting verdict lattice; typed discretion is carried by value-indexed PCAuth witnesses with quorum, delegation, revocation, and timestamps; and legal time is represented by EffectiveDate, Repeal, Toll, and pointwise admissibility-time temporal proposition formers rather than host-language mutation.
The flat admissible fragment is a strongly normalizing calculus of proof terms for finite compliance propositions; extension to holes, tribunals, and time is open. The paper also gives a conditional categorical target in a category with families and a presheaf topos. Its finite cores prove temporal rule-graph non-regression, pack re-evaluation source preservation, quorum extraction, and receipt locality. The structural source relation has weakening, typed substitution, and regularity in generated well-formed contexts. Pure source conversion is confluent. Convertible dependent products have equal stored rows and convertible components. Finite traces of the specified fourteen-rule relation retain their assigned types. Full operational preservation, symbolic execution confluence, unconditional progress, full-fragment normalization, adequacy, and full abstraction remain open.
The principal open obligations are as follows. The full modal and dependent fragment still needs complete normalization, confluence, and type-soundness proofs; the current mechanization should be made fully constructive; and the semantics of re-evaluation under witness revocation and pack evolution need to be closed.
A typed discretion hole records an unresolved judgment, its answer type, and the authority allowed to supply it. Evaluation resumes when the exact request receives an admitted witness. The trace retains both the mechanical derivation and the authorized decision.
References
Abadi, M., Burrows, M., Lampson, B., and Plotkin, G. (1993). “A Calculus for Access Control in Distributed Systems.” ACM Transactions on Programming Languages and Systems, 15(4), 706-734.
Alur, R. and Henzinger, T.A. (1994). “A really temporal logic.” Journal of the ACM, 41(1), 181-203.
Araszkiewicz, M. and Zurek, T. (2015). “Comprehensive Framework Embracing the Complexity of Statutory Interpretation.” In Legal Knowledge and Information Systems: JURIX 2015, IOS Press.
Ashley, K.D. (1990). Modeling Legal Argument: Reasoning with Cases and Hypotheticals. MIT Press.
Ashley, K.D. and Brüninghaus, S. (2009). “Automatically Classifying Case Texts and Predicting Outcomes.” Artificial Intelligence and Law, 17(2), 125-165.
Austin, T.H. and Flanagan, C. (2012). “Multiple Facets for Dynamic Information Flow.” In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012). ACM.
Belnap, N.D. (1977). “A Useful Four-Valued Logic.” In J.M. Dunn and G. Epstein (eds.), Modern Uses of Multiple-Valued Logic, 8-37. D. Reidel.
Bench-Capon, T.J.M. (2003). “Persuasion in Practical Argument Using Value-Based Argumentation Frameworks.” Journal of Logic and Computation, 13(3), 429-448.
Bench-Capon, T.J.M. and Sartor, G. (2003). “A Model of Legal Reasoning with Cases Incorporating Theories and Values.” Artif. Intell. Law, 11(2-3), 97-143.
Bernardy, J.-P., Jansson, P., and Paterson, R. (2010). “Parametricity and Dependent Types.” In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), 345-356. ACM.
Bernstein, D.J., Duif, N., Lange, T., Schwabe, P., and Yang, B.-Y. (2012). “High-Speed High-Security Signatures.” Journal of Cryptographic Engineering, 2(2), 77-89.
Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., and Zanella-Beguelin, S. (2016). “Formal Verification of Smart Contracts.” In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS 2016). ACM.
Birkhoff, G. (1948). Lattice Theory. American Mathematical Society.
Bradley, A.R. and Manna, Z. (2007). The Calculus of Computation: Decision Procedures with Applications to Verification. Springer.
Brewka, G. (1991). “Cumulative Default Logic: In Defense of Nonmonotonic Inference Rules.” Artificial Intelligence, 50(2), 183-205.
Denning, D.E. (1976). “A Lattice Model of Secure Information Flow.” Communications of the ACM, 19(5), 236-243.
Dinesh, N., Joshi, A., Lee, I., and Sokolsky, O. (2008). “Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking.” In Deontic Logic in Computer Science (DEON 2008), Springer LNCS 5076.
Dworkin, R. (1977). Taking Rights Seriously. Harvard University Press.
Dworkin, R. (1986). Law’s Empire. Harvard University Press.
Dybjer, P. (1996). “Internal Type Theory.” In Types for Proofs and Programs, 120-134. Springer LNCS 1158.
Emerson, E.A. and Clarke, E.M. (1982). “Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons.” Science of Computer Programming, 2(3), 241-266.
Garg, D. and Pfenning, F. (2009). “A Logical Framework for Justified Belief.” Technical Report CMU-CS-09-151, Carnegie Mellon University.
Governatori, G. (2005). “Representing Business Contracts in RuleML.” International Journal of Cooperative Information Systems, 14(2-3), 181-216.
Governatori, G., Antoniou, G., Maher, M.J., and Billington, D. (2000). “A Flexible Framework for Defeasible Logics.” In Proceedings of AAAI 2000. AAAI Press.
Haber, S. and Stornetta, W.S. (1991). “How to Time-Stamp a Digital Document.” Journal of Cryptology, 3(2), 99-111.
Hart, H.L.A. (1961). The Concept of Law. Oxford University Press.
Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., and Rosu, G. (2018). “KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine.” In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF 2018). IEEE.
Hofmann, M. and Streicher, T. (1998). “The Groupoid Interpretation of Type Theory.” In G. Sambin and J. Smith (eds.), Twenty-Five Years of Constructive Type Theory, 83-111. Oxford University Press.
Jacobs, B. (1999). Categorical Logic and Type Theory. Elsevier.
Johnstone, P.T. (1982). Stone Spaces. Cambridge University Press.
Leroy, X. (2009). “Formal Verification of a Realistic Compiler.” Communications of the ACM, 52(7), 107-115.
Levi, E.H. (1949). An Introduction to Legal Reasoning. University of Chicago Press.
Libal, T. and Steen, A. (2019). “NAI: Towards Transparent and Usable Semi-Automated Legal Analysis.” In Proceedings of the Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (ARCADE 2019).
Levy, P.B. (2006). “Call-by-push-value: Decomposing call-by-value and call-by-name.” Higher-Order and Symbolic Computation, 19(4), 377–414. https://doi.org/10.1007/s10990-006-0480-6.
Lorgat, R. (2026a). The Sovereign Jurisdiction Network. Accompanying manuscript.
Lorgat, R. (2026b). How Compliance Composes. Accompanying manuscript.
Lorgat, R. (2026c). Op: Compliance-Carrying Operations. Accompanying manuscript.
Lorgat, R. (2026d). The Lex Artifact: Rocq Mechanization. Portable proof supplement at supplements/lex-proof-supplement.zip, relative to this PDF. Section 11 gives its digest, recorded checks, and scope. A persistent public archive with an immutable identifier remains required for archival reproduction.
Lorgat, R. (2026e). Accession Networks. Accompanying manuscript.
Lorgat, R. (2026f). Recourse. Accompanying manuscript.
Lorgat, R. (2026g). Op Finite Compiler Reference Model. CompilationSoundness.v. https://github.com/momentum-sez/op/blob/develop/formal/coq/CompilationSoundness.v. Inspected 5 September 2026 (UTC). This branch URL is mutable.
Manna, Z. and Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems. Springer.
Martin-Löf, P. (1984). Intuitionistic Type Theory. Bibliopolis, Naples. Notes by G. Sambin from lectures given in Padua, June 1980.
McCarthy, J. (1980). “Circumscription: A Form of Non-Monotonic Reasoning.” Artif. Intell., 13(1-2), 27-39.
McCarty, L.T. (1989). “A Language for Legal Discourse.” In Proceedings of ICAIL 1989. ACM.
McDermott, D. and Doyle, J. (1980). “Non-Monotonic Logic I.” Artif. Intell., 13(1-2), 41-72.
Merigoux, D., Chataing, N., and Protzenko, J. (2021). “Catala: A Programming Language for the Law.” Proceedings of the ACM on Programming Languages, 5(ICFP), Article 77, 77:1-77:29.
Miller, M.S. (2006). Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University.
Nanevski, A., Pfenning, F., and Pientka, B. (2008). “Contextual Modal Type Theory.” ACM Transactions on Computational Logic, 9(3), Article 23, 23:1-23:49.
OASIS. (2013). “LegalRuleML Core Specification Version 1.0.” OASIS Standard.
OASIS. (2018). Akoma Ntoso Version 1.0. Part 1: XML Vocabulary. OASIS Standard, 29 August 2018.
Pfenning, F. (2001). “Intensionality, extensionality, and proof irrelevance in modal type theory.” In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001). IEEE.
Pfenning, F. and Davies, R. (2001). “A Judgmental Reconstruction of Modal Logic.” Mathematical Structures in Computer Science, 11(4), 511-540.
Plotkin, G.D. (1977). “LCF Considered as a Programming Language.” Theoretical Computer Science, 5(3), 223-255.
Pnueli, A. (1977). “The Temporal Logic of Programs.” In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), 46-57. IEEE.
Pnueli, A., Siegel, M., and Singerman, E. (1998). “Translation Validation.” In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1998), Springer LNCS 1384.
Pottier, F. and Simonet, V. (2003). “Information Flow Inference for ML.” ACM Transactions on Programming Languages and Systems, 25(1), 117-158.
Prakken, H. and Sartor, G. (1997). “Argument-Based Extended Logic Programming with Defeasible Priorities.” Journal of Applied Non-Classical Logics, 7(1-2), 25-75.
Reiter, R. (1980). “A Logic for Default Reasoning.” Artif. Intell., 13(1-2), 81-132.
Reynolds, J.C. (1983). “Types, Abstraction and Parametric Polymorphism.” In Information Processing 83, IFIP, pp. 513-523. North-Holland.
Sabelfeld, A. and Myers, A.C. (2003). “Language-Based Information-Flow Security.” IEEE Journal on Selected Areas in Communications, 21(1), 5-19.
Sangiorgi, D. (1998). “On the Bisimulation Proof Method.” Mathematical Structures in Computer Science, 8(5), 447-479.
Sartor, G. (2005). Legal Reasoning: A Cognitive Approach to the Law. Springer.
Satoh, K., Asai, K., Kogawa, T., Kubota, M., Nakamura, M., Nishigai, Y., Shirakawa, K., and Takano, C. (2011). “PROLEG: An Implementation of the Presupposed Ultimate Fact Theory of Japanese Civil Code by PROLOG Technology.” In JSAI-isAI 2010, Springer LNAI 6797.
Seely, R.A.G. (1984). “Locally cartesian closed categories and type theory.” Mathematical Proceedings of the Cambridge Philosophical Society, 95(1), 33-48.
Vákár, M. (2016). “An Effectful Treatment of Dependent Types.” arXiv:1603.04298, version 1. https://arxiv.org/abs/1603.04298v1.
Wadler, P. (1989). “Theorems for Free!” In Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture (FPCA 1989). ACM.
Werner, B. (1997). “Sets in types, types in sets.” In Theoretical Aspects of Computer Software (TACS 1997), Springer LNCS 1281.
Wolper, P. (1983). “Temporal Logic Can Be More Expressive.” Information and Control, 56(1-2), 72-99.
Wong, M.W., et al. (2022). “Overview of the CCLAW L4 project.” In Workshop on Programming Languages and the Law (ProLaLa 2022), co-located with POPL 2022.
BVI Financial Services Commission, BVI Business Companies Act, Revised Edition 2020, ss.109 and 113; Amendment Act 2024, s.21; S.I.75 of 2024.↩︎
Companies Act 2006, s.442, including s.442(5A).↩︎
Pakistan Code, Ministry of Law and Justice, Limitation Act 1908, ss.4 and 14 and First Schedule Art.115.↩︎