1.1 The mathematical question and its scope

Lattice models of access control combine graded information under restrictions [12, 13, 14]. This paper uses their established order-theoretic methods. The added modeling problem is the family of evaluations by different authorities, together with the rules for carrying their evidence between jurisdictions. Section 9.1 gives the detailed correspondence. Birkhoff [3] and Davey and Priestley [6] give the classical lattice facts. The contribution is their application with explicit source records, applicability determinations, recognition obligations, and local decisions.

Two consequences sharpen this construction. First, a grade check commutes with composition exactly when its accepted states have a least threshold (Proposition 4.7). The same condition classifies maps into ordered tiers (Theorem 6.3). Second, recognition cannot raise derived evidence above the least upper bound of its original sources (Proposition 5.15). These are grade guarantees. Permission additionally requires compatible current witnesses and the reserved local decision.

1.2 Notation

The order notation records which grades support which comparisons. A partially ordered set, or poset, allows two grades to be incomparable. A chain is a poset in which every pair can be compared. The meet is the greatest common lower bound, and the join is the least common upper bound. In a chain they are minimum and maximum. The definitions below also cover domains with several independent requirements.

We write [n]\coloneqq\{1,2,\ldots,n\}. A bounded lattice is a poset with binary meets \wedge and joins \vee, a least element \bot, and a greatest element \top; it is complete if arbitrary meets and joins exist, and every finite lattice is complete. An up-set U\subseteq L satisfies: a\in U and a\leq b imply b\in U. The principal filter of a is \uparrow\!a\coloneqq\{x\in L:x\geq a\}. For a,b in a finite distributive lattice, the set \{c:a\wedge c\leq b\} has a largest element, the residual a\to b, characterized by a\wedge c \;\leq\; b \iff c \;\leq\; a\to b; a bounded distributive lattice with all residuals is a Heyting algebra, and we write \neg a\coloneqq a\to\bot for the pseudocomplement. A map F between lattices is monotone if a\leq b implies F(a)\leq F(b), and meet-preserving if F(a\wedge b)=F(a)\wedge F(b).

2.1 Why the meet is forced on applicable grades

Three conditions express what cross-authority composition must do. Idempotence says that repeating one evaluation changes nothing. Monotonicity says that improving every input cannot worsen the result. The never-weaker condition says that the result is below every participating verdict. The last condition is imposed by the legal effect of each participating rule: a clearance elsewhere does not cure a violation here.

Every hypothesis is necessary. Without idempotence, the constant \bot operation is monotone and never weaker. Without monotonicity, on 0<1<2 one may set 1\star2=2\star1=0 and take the minimum on all other pairs. Without never-weaker, the join is idempotent and monotone. On the three-grade chain the proposition yields the familiar facts: a violation survives, full compliance is neutral, and a repeated check changes nothing. Associativity and commutativity follow because the operation is the meet.

2.2 Why five outputs do not close

A total operation on the five inputs of Definition 2.1 would need to preserve an applicable grade and the fact that another authority did not apply the domain. The following result shows that the five-element carrier cannot do so.

For example, combine a Pending evaluation with a NotApplicable determination. None of the five input labels records both facts. We therefore store a pair: the combined applicable grade and the set of scope markers received. The added symbol \top in the first component means that no applicable grade has been supplied. It acts as a neutral value when a later applicable evaluation arrives. The notation 2^X denotes all subsets of a set X.

Let G_\top=\{\mathrm N<\mathrm P<\mathrm C<\top\} and set \mathcal R=G_\top\times2^{\{\mathrm{NA},\mathrm E\}}, \qquad (g,S)\sqcap(h,T)=(\min(g,h),S\cup T). The intended readings embed into \mathcal R by \iota(\mathrm{App}(g))=(g,\varnothing),\qquad \iota(\mathrm{NA})=(\top,\{\mathrm{NA}\}),\qquad \iota(\mathrm E)=(\top,\{\mathrm E\}).

The theorem asks for less than a semilattice: commutativity and idempotence are not needed. The obstruction is the carrier, not a missing law.

There are four possible grade entries and four possible marker sets. All sixteen pairs are needed if the empty collection is permitted. The reverse-inclusion order on marker sets makes their union a meet: combining restrictions retains every observed marker. A nullary meet means the meet of an empty family, which supplies the neutral record.

A mixed value such as (\mathrm P,\{\mathrm{NA}\}) says exactly what happened: among the authorities that applied the domain, the aggregate grade is Pending, and at least one authority found the domain outside scope. A reporting system may order these records for display. That diagnostic order is not a compliance order and cannot define admission, join, or implication.

Elimination means resolving the applicability disagreement into a usable verdict. It is an act of authority. A mixed result becomes an executable verdict only when a named rule-layer authority determines how the applicability disagreement affects the act in question. An algebraic projection cannot supply that determination.

2.3 Source cells before aggregation

Suppose one authority returns \mathrm{App}(\mathrm N) and another returns \mathrm{NA} for the same domain. Their exact aggregate is (\mathrm N,\{\mathrm{NA}\}). A local display may show NonCompliant, but that display cannot recover the second authority’s scope judgment. Transport must therefore receive the source cells before aggregation.

Even the exact pair omits which authority supplied each component. That information matters when a destination recognizes one source or when a later rule changes the permitted use of its determination. We call an individual attributable evaluation a source cell. The aggregate is a query on those cells, not their replacement.

For a family S in one domain, let v_s\in V denote each cell’s value. Its mixed summary is Q(S)=\mathop{\sqcap}_{s\in S}\iota(v_s). Families merge by compatible map union. The union retains every source record, including the records already represented in another family. Transport retains the original family and appends its treatment as evidence support. This support uses a separate copy of the grade lattice. An applicable source verdict contributes to the restriction meet. An admitted supporting assertion can also contribute to an evidence join. The latter records combined support and leaves the source verdict and scope intact. Section 5.5 defines that evidence use.

The intake type accepts the attributable family and its derivation. A five-label aggregate alone has a different type. It cannot supply a complete cross-authority family, by Theorem 2.3. An authorized applicability decision cites the cells it resolves and records the decision separately. Both original scope judgments remain available for another request under another destination’s law.

2.4 Sanctions and the applicability axis

Sanctions clearance is re-evaluated at the destination unless a legal instrument expressly names a shared authority. A clearance record binds the list, list version, screening rule, aggregation rule, transaction context, and evaluation time. The destination may rely on that record only where its own law permits and only to the extent that its governing list coincides. A NonCompliant sanctions grade remains absorbing under the meet. The applicability record remains explicit when authorities disagree about whether their sanctions law reaches the act.

3.1 Compliance domains

The previous section combined authorities’ answers to one question. A request usually has several questions, with different useful grade scales. Anti-money-laundering checks, abbreviated AML, can distinguish levels of evidence. A sanctions check can instead use two grades. These scales are specified by an adopted rule pack, the versioned rules and interpretations defined in Appendix A.1.

A single domain can also require several kinds of support. For the Sharia example, the rule pack specifies screens concerning interest (riba), contractual uncertainty (gharar), and gambling (maysir), as well as asset backing and board certification. These are separate questions within that illustrative domain.

The order also answers a conditional comparison: which grades c can be combined with a while keeping the result below b? The largest such c is the residual a\to b. Its existence explains the additional Heyting structure used below. It is an operation on grades, rather than an authority to infer a legal permission. Distributivity permits the candidate solutions to be joined without losing their defining property.

3.2 The product

Record the answer to each regulatory question in one coordinate. Comparing two records then means comparing every corresponding answer. This construction permits the same meet rule to apply across different grade vocabularies without comparing an AML grade to a sanctions grade.

The order reads operationally: a\leq b says b is at least as compliant as a in every domain, the meet is the pointwise weaker state, and the join is the pointwise stronger one. The main instance is \mathcal{L}_{23}, the product of the factor family in Appendix A.

The resulting operations can all be calculated within individual domains. The proposition verifies that those calculations retain the order laws needed for the later threshold and recognition arguments.

3.3 Correlated domains and the valuation map

The coordinatewise product is a modeling choice, and real compliance data need not respect it. Sharia and Insurance couple through riba-sensitive insurance structures; AML and DataPrivacy pull against each other when reporting obligations create cross-border data-transfer exposure; AntiBribery and Licensing couple when discretionary licensing practices create payments that anti-bribery controls reject. These are correlations between the grades assigned to different coordinates, and they do not change the algebra of \mathcal{L}_n.

For example, a summary might take one coordinate from each of two incompatible accounts of the same instrument. The resulting vector can exist in the product even though the evidence supports neither combined account. We therefore distinguish a concrete witnessed state from its grade vector. A witness is the retained evidence and checked derivation that support a state in the specified request context.

Fix a request q and an authority context \sigma. Let \mathcal{M}_{q,\sigma} consist of witnessed states that satisfy the applicable cross-domain constraints. Each state records its original assertions, checked derivations, applicability determinations, and dependencies. Its valuation v:\mathcal{M}_{q,\sigma}\to\mathcal{L}_n assigns the supported grades. Membership in \mathcal{M}_{q,\sigma} includes joint admissibility as defined below. It does not itself supply a local permission.

A set of witnessed states represents genuine alternatives. Its image under the valuation keeps their grade alternatives separate. The maps \alpha and \gamma below pass between these two descriptions. The transition relation T records which concrete successors are permitted by a specified construction. Its abstract counterpart lists the grades of those successors.

This abstraction keeps alternatives separate. A cheaper summary retains only \bar\alpha(X)=\bigvee_{m\in X}v(m). With \bar\gamma(c)=\{m:v(m)\leq c\}, the same calculation gives \bar\alpha(X)\leq c if and only if X\subseteq\bar\gamma(c). The summary is an upper bound and need not be attained. In two binary domains, concrete alternatives (1,0) and (0,1) have summary (1,1) even when no concrete state has that grade.

An executable grade therefore carries a witness m\in\mathcal{M}_{q,\sigma} with v(m)=c, or a checked concrete construction producing such a witness. Ambient meet, join, and recognition operations remain available for bounds and planning. Their use as executable state transitions requires a concrete lifting relation T. Closure of realizable states under every ambient operation is not assumed. When independent compatible assertions supply the two coordinates, their checked joint derivation can produce a witness for (1,1). The local decision then uses that witness under its current guards.

3.4 Which operations a map preserves

A map can preserve some grade calculations and fail to preserve others. A morphism means a map that preserves the operations specified by the category under discussion. Here a category consists of objects and such maps, with associative composition and identity maps. The product property says that specifying all coordinate maps determines exactly one map into the product.

This distinction matters when transferring calculations. A map preserving meet and join need not preserve the residual. Corridor maps introduced later assume only monotonicity and deflationarity, so they need not be morphisms for either structure considered in the following remark.

4.1 The multi-harbored entity

Fix one request evaluated in several jurisdictions. We call each jurisdiction in that family a harbor. The term names an evaluation context and makes no claim about an entity’s legal status there. The composed state retains the weakest applicable grade in each domain.

In \bigwedge_j x^{(j)}, a record with no restriction in a coordinate uses \top there, because meet with \top leaves the other value intact. Later, a record contributing no evidence uses \bot, the neutral value for join. These padding conventions describe different uses of a vector.

An entity graded in a single domain i at grade g is the vector with g in coordinate i and \top elsewhere; meets of such vectors produce every state, so per-domain records and per-harbor vectors are two presentations of the same data. Combining two abstract entity records merges harbor sets and takes the meet of composed states, so multi-harbored entities are closed under composition as abstract records. Executing a legal merger also requires a concrete witnessing construction as in Proposition 3.9.

4.2 Admissibility surfaces are up-sets

The composed vector still needs a rule that decides whether its grades are sufficient for the requested instrument. Call the accepted set an admissibility surface. We assume that stronger admissible evidence cannot fail a grade requirement already satisfied. This assumption fixes the request, rules, and evidence compatibility. It says nothing about a later revocation or a changed local decision.

The threshold example has a least accepted vector. The next lemma shows that every finite accepted set closed under meet has such a least member. That fact will characterize both binary grade checks and ordered tiers.

A compatible check gives the same answer whether we first combine the grades or first check each grade and combine the answers. The next proposition shows exactly when this interchange is valid.

4.3 Compound surfaces: the boundary

A rule can offer alternative ways to pass. One state may satisfy its first alternative while another satisfies its second. Their common lower bound may satisfy neither. The following illustrative predicate shows why monotonicity suffices for conservative composition but does not give exact compatibility. It defines a mathematical test, not an operative sanctions rule.

4.4 Multi-harbor composition

We now combine the requirements themselves. Requiring every harbor’s grade check means intersecting their accepted sets. This operation works for all monotone checks, including the compound check above.

The pointwise meet is deliberately unforgiving. For any two harbors grading the same domain, the composed state carries the weaker grade. In a factor whose bottom is \mathrm{NotRecognized}, for example, \mathrm{FullyCertified}\wedge\mathrm{NotRecognized} =\mathrm{NotRecognized}. A harbor that refuses to recognize a certification collapses that coordinate of the composed state regardless of certifications held elsewhere.

5.1 Corridor edges

The record has four components. It lists the domains whose evidence can travel, the map applied in each such domain, the domains evaluated afresh, and the governing clauses. A carried domain may also require a fresh evaluation. For example, carried licensing evidence can inform the destination’s own licensing assessment (Section 5.6).

The map \phi_{A\to B,i} gives the exact content of a domain’s recognition grade. Full means the identity map. Partial means a declared non-identity deflationary map. Conditional means that a named carriage predicate enables the declared map in the fixed request and use context. Only clauses expressly designated as carriage prerequisites guard this import. An identity-on-success map is one conditional profile; a guarded discount retains its declared map. A resolved false prerequisite supplies no admitted transported witness. Its evidence summary is bottom for a resolved map comparison. An unanswered prerequisite or unavailable comparison embedding remains unresolved and does not become bottom in that comparison. A comparison embedding supplies the agreed interpretation on the common grade scale. Fresh local questions remain obligations of their receiving authority. Imported evidence can inform a still-pending local question. Its answer becomes a carriage prerequisite only when the governing instrument expressly requires that ordering. Import itself preserves the local decision, and execution still checks every applicable clause. None means i\notin C_{A\to B}. These labels classify a signed map and its conditions. They do not replace either.

Monotonicity says better origin evidence never transports worse. Deflationarity says a treaty cannot manufacture evidence: a recognition map may discount a grade or carry it intact, never raise it, and in particular \phi_i(\bot)\leq\bot forces \phi_i(\bot)=\bot — absent evidence transports to absent evidence. Deflationarity is the condition conservativity runs on (Proposition 5.15): monotonicity with \bot-preservation alone would admit a map sending an intermediate grade to \top, a treaty that grades an entity above its evidence.

5.2 Corridor composition

Suppose evidence travels from A through B to C. A domain survives only if both legs carry it. Its grade undergoes the first treatment and then the second, while all evaluation obligations remain. Below, A\to C denotes this computed composite. An independently declared direct corridor with those endpoints may have different terms.

Associativity means that grouping a route into segments does not change its computed record. The identity record describes a route of length zero. These are the two composition laws needed to regard corridors as the maps in a category.

A network in which every jurisdiction maintains at most k treaty partners carries at most k\,|\mathcal{J}| directed corridors — at most k|\mathcal{J}|/2 partnerships, two directions each — linear in the number of jurisdictions.

5.3 Corridor labels

Registries and reports sometimes need a compact account of transport: which domains a corridor carries, and how faithfully. The label below forgets the fresh-evaluation mask M and the clause set \Gamma. It is therefore a transport summary, not a complete corridor record.

These labels support set-like calculations on transport summaries. Here the order on carrying sets is ordinary inclusion. The two-element symbol \Gamma denotes fidelity in this subsection, whereas a subscripted \Gamma_{A\to B} still denotes the corridor’s clause set.

Composed labels never over-report a route. A one-symbol summary forgets whether a leg’s discount lies in the surviving carrying set. The leg-by-leg summary can therefore look more discounted than the route, but never less. Per-domain fidelity composes exactly. A composite map is the identity at a carried domain precisely when both leg maps are. A first-leg discount survives the deflationary second leg because \phi_{B\to C,i}(\phi_{A\to B,i}(g)) \leq\phi_{A\to B,i}(g). A second-leg discount composed with the identity is itself.

5.4 Transport of states

Apply a corridor to an evidence vector. Each carried coordinate receives its declared treatment. An uncarried coordinate contributes no evidence, so its transported value is \bot. The term functorial below means that applying two successive transports agrees with applying their computed composite, and that the identity corridor changes nothing.

Transporting a source state along a chain of corridors is therefore the same as transporting it along the composite corridor. This functorial statement concerns carried evidence only. It does not erase the fresh evaluations that an intermediate authority adds.

5.5 Recognition updates, and conservativity

Transport delivers evidence. A destination can combine a recognized file with its existing support. This operation uses join in the evidence copy of the lattice. The earlier meet combines applicable restrictions. The two operations answer different questions, and neither operation issues a local permission.

The next definition relates the records already introduced. A source cell records an authority’s evaluation. An evidence record retains a typed assertion, and a derivation records how assertions support a grade. The witness set contains the exact records used for one decision. Its issue anchor records the original issuance reference. A later transport receipt preserves that reference and the original use interval.

5.6 Complete route contracts

Consider a destination that reuses an identity file and performs its own licensing assessment. Identity evidence travels in the licensing domain, which also remains in the fresh-evaluation set. Authorized licence issuance creates a reporting duty with a deadline. Another route can return the same grade while requiring a different report. Equality of grades then fails to describe equality of the resulting institutional states.

The fresh mask is the domain projection of fresh-evaluation obligations. Carriage prerequisites state what permits import. Fresh questions state what their named destination must evaluate. A question becomes an import prerequisite only when its instrument imposes that order. The contract therefore permits import while the destination’s evaluation remains pending. A declared conditional discount uses its declared grade map when the prerequisite holds.

Write K=(k_1,\ldots,k_m) for an ordered route of complete contracts. Adjacent endpoints must agree. Every edge binds the same immutable request, act, subject, and purpose, together with its own local context. The route retains all edge contexts and authority records. Its grade projection composes the maps on the intersection of carrying sets. Its obligation projection retains the compatible union of instantiated obligations, including obligations owned by intermediate destinations.

A route receipt retains the original attributable cell family, its current per-cell treatments, the ordered contracts, and those obligations. Composition concatenates contract sequences. It preserves original cell bodies and applies each next treatment to the current grade. Pending questions and completed answers keep their owning authorities. An obligation changes status only through its named completion rule. Permission checks the prerequisites of the named stage. A later reporting duty remains outstanding after an authorized act that creates it. Every traversal has its own request-bound identity. Retrying that traversal retains its result. A later traversal can use the same policy again.

The producer and consumer may use two different formats for the same contract. The inverse conversion matters at that boundary: the receiver can recover local questions, authority, and duties as well as the grade maps.

This theorem concerns the complete declared records. It does not infer an institution’s legal meaning from unsigned field names. Adoption of a record and semantic adequacy of the encoded instrument remain named premises. A reduced carrying-set view is a useful projection of this contract. It does not determine its omitted local questions or duties.

5.7 Equivalence of running routes

Complete-record conversion preserves one declared contract. Two running routes can instead have different internal records yet respond identically to every admitted event sequence. To compare that behavior, retain the outputs that matter to the relying institution, including duties and deadlines. The finite machine below makes those observable outputs explicit. Its transition function \delta returns the next state, and o returns the observation emitted for an event. The finite alphabet is part of the declared model. Actual timestamps and evidence records require a separate justified reduction before they fit this finite comparison.

For machines A,B over this alphabet, explore the product of reachable state pairs, beginning at (s_0^A,s_0^B). At each pair, compare both observations for every input. A difference returns the input word that reaches it. Otherwise enqueue the successor pair unless already visited.

This result permits different internal route states. One route can keep an extra cache state while producing the same observations. Conversely, two Allow results differ when one creates a reporting duty and the other does not. Changing only the deadline also distinguishes them. Removing duties from the observation would prove a different, weaker comparison. The finite result leaves unbounded rule-state and nondeterministic environments to simulation or game-based methods. A production compiler must separately establish that its encoded transitions implement the adopted rules and complete observation contract.

6.1 Tier data

6.2 The classification theorem

Top preservation requires the strongest vector to reach the highest tier. The threshold returned by the adjoint is a least grade vector, rather than a least-cost acquisition plan. Repeated thresholds can skip tiers.

The proof reduces each tier to a binary question: is the assigned tier at least this high? Each accepted set then satisfies the principal-filter lemma. Its least vector supplies the required threshold. Nested accepted sets produce thresholds ordered in the opposite direction.

Composition is a meet, and the tier map preserves meets, so tiers compose by minimum and never rise under new obligations. Proposition 5.15 extends the bound to arbitrary sequences of meets, transports, and recognitions: every derived state lies below \bigvee\mathcal{E}, every map in sight is monotone and every transport deflationary, so the tier of any derived state is at most \Phi(\bigvee\mathcal{E}) — the tier the pooled evidence itself warrants — and the tier of the composed state is at most \min_j\Phi(x^{(j)}). This is an evidence-tier bound. The local grade cap can only lower the decision tier. Permission also requires the local decision and current witness guards.

6.3 Join preservation fails

Joining support can cross a threshold that neither input reaches. For example, one record can supply the first required domain and another the second. Their tiers conceal that complementary evidence. The next result shows why the classification preserves meet but can fail for join.

In the following remark, composition means the combination of cross-authority verdicts. Recognition and independent evidence planning use the separate evidence join.

8.1 Resource limits and incremental reuse

A bounded search reports one of four results: an optimum with a matching certified lower bound; infeasibility with exhaustive search or a checked certificate; a feasible incumbent with incomplete search; or unknown. Unknown means that no feasible incumbent or infeasibility certificate has been established. Nonnegative costs always give lower bound zero. A timeout supplies neither optimality nor infeasibility. Every result binds the request, context, catalogues, costs, constraints, and guards. It records consumed resources and the gap between available bounds.

Cached feasibility requires current guards for every retained witness, derivation, and duty. Revocation or changed source ownership invalidates dependent results. Optimality also depends on unused alternatives and their costs. A cheaper new offer can invalidate optimality while the incumbent remains feasible.

An exact incremental method stores offer-prefix dynamic-programming layers, with each layer considering inclusion or exclusion of one offer. After the first changed offer, it recomputes that layer and the remaining suffix. Earlier layers remain reusable only when requirements, costs, offer semantics, and constraints agree. A changed target needs a rebuilt encoding or an exact correspondence between the old and new states. Each retained layer has at most 2^r entries. Storing all prefixes costs O(m2^r) memory; retaining fewer checkpoints trades memory for recomputation.

8.2 Finite benchmark

The measurements below concern a fixed synthetic catalogue. Dynamic programming, abbreviated DP, stores the least cost for each coverage state. Resident set size, abbreviated RSS, measures process memory. These measurements compare the finite methods just described and test the distinct evidence and duty cases.

A deterministic synthetic set contains seven coverage instances and ten semantic fixtures. Exact dynamic programming supplies the coverage optima, and finite enumeration evaluates the semantic fixtures. The comparison uses Python 3.14.6 and SciPy 1.17.1 on macOS 26.2, with three fresh-process samples per row. All 33 incumbent-bearing rows pass exact integer feasibility and cost checks. The full record contains 44 rows and 132 samples.

Table 1 reports the 12-domain, 24-offer instance with seed 31. Elapsed time excludes imports. Python allocation peaks exclude native solver memory; process RSS includes those allocations and imports. The observed gap is measured against the exact dynamic program. Numerical solver bounds remain separate from exact certificates.

The constructed greedy example costs 6 against an optimum of 5. Joint-input transport reaches its target at cost 3, while the separate transport catalogue is infeasible. Conflicting support, duplicate origins, a reserved refusal, an unresolved judgment, a local cap, and revocation each prevent the corresponding invalid plan.

After revocation, incremental recomputation uses 512 transitions against 2,210 for full recomputation. Adding a cheaper offer uses 512 against 2,722. Cached-prefix construction is excluded from update time and remains part of the initial computation. A zero-work limit returns Unknown. A 16-pair limit finds a checked incumbent and returns feasible with incomplete search and exact lower bound zero. These measurements describe the declared finite instances, with no inference about deployment scale.

9.1 Lattice models of graded labels in access control

The modeling decision made here — grade an object in a finite lattice, and let a lattice operation compute the grade of a combination — is the standing model of security classes in access control. The correspondence is close, and it runs in both directions.

Denning [12] takes a finite set of security classes ordered by a can-flow relation, with a lower bound and a total class-combining operator, and derives that the classes form a bounded lattice in which the class of a combination is the join of the classes combined. Read Denning’s “more restricted” as this paper’s “less evidence”, so that the order reverses, and four correspondences are exact. Denning’s combining operator is the meet of Definition 4.1 — pointwise here because \mathcal{L}_n is a product, where his security classes carry no product presentation in general — and his consequence that a combination is never less restricted than any input is Proposition 4.9 together with Corollary 4.10: no combination is graded above its evidence. His derivation of the lattice from finiteness and a combining operator, rather than a choice of one, is the antecedent of Remark 3.10, and his military example — a chain of clearance levels paired with a set of categories, ordered and combined componentwise — is a two-factor instance of Definition 3.7, non-Boolean for the reason Remark 3.10 gives, since its level chain carries intermediate grades.

Bell and LaPadula’s simple security property [13], that a subject may read an object only when its clearance dominates the object’s classification, admits for a fixed object exactly the clearances in a principal filter: the threshold check of Proposition 4.7, in the holder form of Remark 4.11.

Biba’s low-water mark [14] gives a subject that has read an object the meet of the two integrity levels, which, with integrity read as strength of evidence, is the two-harbor composed state.

Role-based models [15] order roles by inheritance and supply no grade-combining operator, so they carry no composition law of this kind.

What that literature does not carry is the indexing, and the indexing is where the results here live. A Denning object holds one label, and the combining operator combines the labels of distinct objects whose contents merge. Here one entity holds a family x^{(1)},\ldots,x^{(k)} over a shared factor family, one member per authority that grades it, and the meet of Definition 4.1 runs across that family rather than along a flow edge. Those models also supply no algebra of grade-lowering maps: declassification sits outside the flow policy as a trusted exception, and Biba’s low-water mark is one fixed rule with no parameters to compose. The corridors of Definition 5.1 put the discount inside the model as deflationary monotone maps with a carrying set, composing associatively with identities (Theorem 5.4) and transporting states functorially (Proposition 5.9). And those models fix a threshold rule rather than classify the available ones, where Theorem 6.3 identifies the maps into a finite tier chain that respect composition with the nested threshold families, and with the maps carrying a unique left adjoint. The lattice facts behind all three remain as classical as the rest of the paper; the compliance model they carry is what is new.

9.2 Order-theoretic foundations

Every lattice-theoretic fact used above is classical: Heyting algebras originate with Heyting [2], the finite-distributive representation with Birkhoff [5, 3], and the textbook treatments of Davey–Priestley [6], Johnstone [7], and Borceux [8] cover residuals, adjunctions, and products. Relaxing the commitments made here — idempotent, commutative, discrete composition — leads to residuated lattices and substructural settings [11, 10, 22]; the present model is deliberately the simplest member of that family.

9.3 Regulatory ontology via description logic

Regulatory ontologies are commonly expressed in description logic, in the OWL 2 profile family [16, 17], with the DL-Lite [18] and EL^{++} [19] profiles carrying large regulatory knowledge bases and OWL RL the profile implementable by rule engines in polynomial time [20]. These are Boolean ontologies: classification is crisp. The present model drops Boolean-ness in favor of graded evidence, accommodating the intermediate and provisional grades regulators routinely use (Example 3.2; SSBPending versus PartiallyCertified in Appendix B). The two framework families are complementary: description logic answers what kind of regulatory object an entity is; the graded lattice answers what state of evidence it exhibits.

9.4 Fuzzy and many-valued reasoning

Fuzzy logic [21, 22] grades membership over [0,1]. The present model chooses finite factors to represent the discrete evidence distinctions selected by a rule pack. Continuous observations can be compared with that pack’s thresholds before composition. Finite chains also give the residual a two-case closed form (Lemma 3.6) where fuzzy negation requires choosing a negator. Theorem 7.2 gives the continuous threshold representation under arbitrary meet preservation.

9.5 Compositional compliance in deployed systems

REALM [23] and LegalRuleML [24] combine regulations by rule-set union. Plutus [25], Algorand’s TEAL [26], and Aave Arc [27] conjoin Boolean gates. In both families, failure is a conflicting rule pair, not a graded below-threshold state. Neither family models compliance as a finite distributive lattice with meet preservation and an adjoint classification. The present problem is different: it composes graded states across jurisdictions by pointwise meet. Section 9.1 states what this paper adds to the access-control use of graded lattices.

Proved in this paper.

Proposition 2.2 forces the meet from one hypothesis set. Theorem 2.3 proves that the five-input carrier cannot retain both axes under a total associative operation. Proposition 2.4 gives the exact finite closure. The product, threshold, corridor-transport, staged-arrival, and tier-classification results follow under their stated finite-lattice and monotonicity hypotheses. Proposition 2.6 preserves source applicability through aggregation. Theorem 5.19 establishes complete-record conversion and contextual composition. Theorem 5.21 decides observational equivalence for finite deterministic route machines. Proposition 3.9 separates grade alternatives from witnessed states. Theorem 7.2 gives the complete-lattice threshold representation. Section 8 establishes exact finite planning and the independent-offer coverage reduction.

Mechanized finite cores.

Three source modules formalize the finite structures named here.

TensorAlignment.v proves the n-ary mixed-axis reduction, agreement on applicable inputs, exact flag reporting, two provenance loss witnesses, and the impossibility core. VerdictHeyting.v formalizes the five-element chain and its Heyting laws.

For normalized snapshots, the checker in CorridorMonotone.v is sound and complete for equality of three lists: carried cells, the fresh evaluation domain, and instrument clauses. Rejection establishes inequality, and coherence is decidable. These checker proofs lie outside the parameterized corridor-history module and do not use its interface assumptions. The separate RuleExtension interface declares a cell-value type, a transition rule, and the axiom rule_step_extends. Single-step and multi-step history monotonicity require that extension premise. Applying the snapshot checker to corridor semantics still requires a justified normalization.

In VerdictHeyting.v, rank declares the order NonCompliant, Pending, NotApplicable, Exempt, Compliant, in that sequence. The definitions compute minimum, maximum, and the chain residual. The theorem verdict_is_heyting proves laws for that chosen chain. It does not retain simultaneous grade and applicability observations. For example, its minimum of Pending and NotApplicable is Pending. The exact record here retains both in (\mathrm P,\{\mathrm{NA}\}). Thus the chain theorem concerns a different operation from the lossless composition ruled out by Theorem 2.3. The open semantic lifts require the richer attributable records.

Sources and reproduction.

The accompanying source supplement contains these proof sources and the historical benchmark records in Section 8.2. Its README specifies dependencies and commands for reproduction from a fresh extraction. Fresh runs write separate output and preserve the historical measurements. The relative archive path and its SHA-256 digest are:

supplements/compliance-composition-supplement.zip
19c13b70d857be315f3c0ae30c9d4c5bd8ad10bb92e477f57ac7c0d2dbf3382f

Conditional consequences.

Recognition conservativity requires monotone, deflationary grade maps. The staged-arrival inequality joins fresh evaluation evidence. Joint admissibility and reserved decisions separately govern permission. The finite tier classification requires a finite state space and meet preservation. The complete-lattice extension requires arbitrary meet preservation. These premises need not hold in every legal regime.

Open problems.

The end-to-end audit theorem must bind every source cell to its authority, rule version, exemption scope, and committed passport root, a cryptographic commitment identifying the exact aggregate evidence record, and must reject every unauthorized elimination from a mixed result. Complete-record normalization preserves the declared fields. The finite route machine proves equivalence of its encoded transitions. The corresponding production result still needs a proved normalization from adopted instruments and refinement of the actual evaluator. Dependent verdicts also require a well-founded domain graph, or a separate fixed-point semantics when legal dependencies are cyclic.

A.1 An authority-owned rule pack

A domain name identifies a question. Its operative meaning comes from an adopted rule for a particular jurisdiction, product, act, and time. A rule pack makes that interpretation explicit.

The active pack is selected by the current governing authority. Evaluation first checks that adoption, mandate, scope, version, and effective interval apply to the request. It then evaluates the declared rules against exact witnesses, records unresolved applicability or judgment, and supplies the local decision construction of Definition 5.12. Missing adoption or an unresolved rule supplies Await, not an implicit default permission. A valid delegated interpretation can be reused under its recorded scope and guards without a new signature on every mechanical calculation.

IFSB-10, Principle 1.2 and paragraphs 20–22, distinguish a board’s mandate, written appointment, operating procedures, and limits of power [29]. These governance provisions motivate explicit authority fields. They do not prescribe this paper’s coordinate names or ranks. The AAOIFI catalogue identifies the relevant standard families [28]; exact operative clauses and their adoption belong to the jurisdiction- and product-specific pack.

The following domain inventory and Sharia tables define an illustrative encoding. Their algebraic properties hold for the stated tables. An operative instantiation supplies the adopted meanings and exclusions required by Definition A.1. In particular, a recognition classification never supplies an adoption or a local decision by itself.

The distinction concerns what a corridor may carry. Entity-intrinsic evidence describes the entity, its controls, or an instrument. A jurisdiction-indexed status exists only under one authority’s law. Broad domains can contain both. For example, corporate governance evidence may travel, while incorporation status does not. A corridor must split such a domain into typed claims before recognizing any part of it. The table suggests claim types for that analysis. An absent recognition rule leaves a required evaluation pending. It does not activate a default transport or permission.

B.1 Sharia constraints SH-01 through SH-05

B.2 The projection to the top-level chain

Each component grade carries a rank in the top-level chain: the best overall grade the instrument could reach if that component were the only constraint. The overall grade is the worst rank across components — the most restrictive constraint governs.

For instance, the table assigns only PartiallyCertified to contractual asset support, even when every other component receives its highest rank. The minimum therefore retains that component’s limit. In the table, NR, SSBP, PC, and FC abbreviate NotRecognized, SSBPending, PartiallyCertified, and FullyCertified.

The ranks encode the illustrative policy. A bottom evidence grade in SH-01 through SH-04 projects to NotRecognized, whatever the board grade. The local decision separately distinguishes missing evidence from an established violation. A missing board (\bot in SH-05) caps the grade at NoSSB: absence of certification, unlike a substantive violation, still outranks NotRecognized in the top-level chain. The example assigns Minor the rank SSBPending, and a conditional board report or merely contractual asset backing caps it at PartiallyCertified; FullyCertified requires the top grade in all five components.

B.3 Lifecycle-dependent tradability

An instrument’s structure, current assets, and lifecycle stage can pose different trading questions. A pattern name alone cannot resolve them. Let P be the active adopted rule pack, and let \ell and z record the instrument’s lifecycle stage and witnessed facts. Its tradability evaluation is \mathrm{Adm}_P(q,\ell,z)\in \{\mathsf{Permit},\mathsf{Refuse},\mathsf{Await}\}. It returns its dependencies and any further duties with the outcome. Its rule clauses specify the relevant assets, receivables, trading terms, mixture conditions, exclusions, and required judgment. A later stage can therefore receive a different lawful outcome under the same rule pack.

The simplified profile below evaluates a composite pattern from its components under one fixed rule. The pattern names serve as labels in that calculation. Structural recursion means applying the rule first to the components and then to the composite they form.