What ships as law

The price map depends on the admissibility surfaces, the mechanized composition core, and sanctions terminality. Each has a distinct proof status.

The companion Composing Compliance Across Jurisdictions establishes the admissibility filter. On the Applicable fragment, each domain factor is a finite distributive lattice. The product over the tensor’s 23 domains, the Applicable-fragment lattice \mathcal{L}_{23}, is also finite distributive. The multi-harbor state is the pointwise meet across harbors. Write S_J for jurisdiction J’s admissibility surface: it maps a state c \in \mathcal{L}_{23} to a verdict in \{0 < 1\}. The state and harbor orders affect these surfaces in opposite directions.

In the state order, S_J is monotone. More evidence never loses admission, so the admitted set U_J = S_J^{-1}(1) is an up-set. A more compliant entity is admitted in at least as many places. This orientation follows the companion’s definition of the admissibility surface.

In the harbor order, composition is antitone. For a harbor set H, the composed surface is S_H = \min_{J \in H} S_J: admission requires every harbor to admit. Thus H \subseteq H' gives S_{H'} \le S_H pointwise. Each additional harbor can only shrink the admitted set, by the companion’s multi-harbor proposition. Greater compliance widens the set of lawful holders, while additional jurisdictional requirements narrow it.

Admission also depends on where each surface is evaluated. An entity has one state per harbor, written x^{(J)} in harbor J. Their pointwise meet is the composed state c^{\mathrm{eff}} = \bigwedge_{J \in H} x^{(J)}. Per-harbor admission evaluates each surface at its own state.

Evaluating all surfaces at c^{\mathrm{eff}} gives a conservative check. Since c^{\mathrm{eff}} \le x^{(J)} and admitted sets are up-sets, success at the composed point implies success at every harbor’s own state. The converse fails, as the companion’s composed-check corollary shows. Per-harbor evaluation determines admission. The composed-point check is a sound approximation.

The composition core is mechanized in Coq in TensorAlignment.v (43 Qed, 0 Admitted, 0 Axiom). It includes the grade-meet laws, the n-ary operator, and the mixed-axis impossibility. The binary meet on tensor factors is tensor_meet, and its n-ary form on the full tensor state space is tensor_meet_all. On non-empty all-Applicable inputs, it agrees with the fragment meet (tensor_meet_all_applicable_fragment). On mixed inputs, it returns a structured meet_result whose flags identify exactly which applicability axes appeared (tensor_meet_all_flags_exact).

The result has eight constructors: MR_Grade, MR_NotApp, MR_Exempt, MR_AppVsNotApp, MR_AppVsExempt, MR_NotAppVsExempt, MR_AppVsNotAppVsExempt, MR_Empty. The four mixed-axis constructors retain the provenance of applicability disagreement across jurisdictions.

The impossibility of collapsing that disagreement to one grade without losing the compliance signal is mechanized at full strength in LatticeOrthogonalFull.v. This standalone Coq artifact contains 29 Qed, 0 Admitted, 0 Axiom. Its theorem heyting_closure_impossible_with_audit_fix ranges over total operations on the five-state cell: Applicable at one of three grades, NotApplicable, or Exempt. The operation must be commutative, associative, and idempotent, and extend the grade meet on Applicable inputs. Under those conditions, it cannot preserve both the Applicable compliance signal against NotApplicable and the orthogonality of NotApplicable to Applicable grades. Signal preservation requires Compliant composed with NotApplicable to differ from NotApplicable. Orthogonality requires NotApplicable composed with a grade to be neither that grade nor Exempt. Every semilattice extension of the grade meet loses one axis, which forces a structured result.

The value-layer companion in TensorAlignment.v is no_total_tensor_factor_meet_preserves_signal_and_orthogonality. It states that no total tensor-factor operator both preserves the Applicable compliance signal against NotApplicable and keeps NotApplicable orthogonal to Applicable grades.

Sanctions terminality supplies the third dependency. A sanctions-bottom result is absorbing under composition. In the Op development, ComplianceContext.v proves sanctions_bottom_cannot_become_compliant_after_meet (36 Qed, 0 Admitted, 0 Axiom, 0 Parameter — unconditional). The related verdict_preservation_sanctions result in CompilationSoundness.v is Qed-closed but parametric over the abstract host primitive host_sanctions. Its status is Qed-closed-modulo-abstract-host.

Both surface orientations come from Composing Compliance Across Jurisdictions: monotonicity of S_J in the state order and antitonicity of S_H in the harbor order. That paper defines the surface as a monotone map with an up-set of admitted states and proves S_H=\min_{J\in H}S_J. The shorter note titled How Compliance Composes gives the lattice construction and mixed-axis dichotomy with the same Coq citations. It defines no admissibility surface and is therefore not the source for either orientation.

Neither orientation is a theorem in either .v file. Those files establish the grade-meet laws, n-ary composition, and impossibility, but no threshold-surface theorem. Their status is “paper-proved over the mechanized meet,” as used throughout this paper.

The typed price map

The price map takes three typed inputs and returns either a price or a typed obstruction:

w \;:\; \mathrm{PDCF} \,\times\, \prod_{J \in H} \mathrm{TF}^{\mathcal{D}} \,\times\, \mathrm{Belief} \;\longrightarrow\; \mathrm{Price} \,\sqcup\, \mathrm{PriceObstruction},

Here \mathcal{D} indexes the tensor domains, and \mathrm{TF} is the tensor-factor type of the mechanized core. Each domain carries an Applicable grade, NotApplicable, or Exempt.

The first argument is the instrument’s intrinsic present-discounted cash flow: the \Phi-valuation of the claim program in Intelligent Assets. Face value, coupon schedule, default waterfall, and risk-neutral expectation derive from it. This input uses standard finance.

The second argument is the entity’s attested compliance record: one tensor-factor vector per harbor, x = (x^{(J)})_{J \in H}. Its entry x^{(J)}_d is the factor on domain d attested in harbor J. On the Applicable fragment, every coordinate carries a grade and x^{(J)} lies in \mathcal{L}_{23}. By construction, the input is this attested record. A caller cannot supply an unfiltered compliance state.

The map uses two objects derived from the record. The first is the composed vector T_H(x) \in \mathrm{MeetResult}^{\mathcal{D}}. On each domain d, T_H(x)_d applies tensor_meet_all to the per-harbor factors (x^{(J)}_d)_{J \in H} and returns one of the eight meet_result constructors. This vector determines the branch: it detects mixed applicability, uniform exclusion from scope, and an empty harbor set. On a homogeneous in-scope domain, it carries the composed grade.

Let \Pi_{\mathrm{App}} return the grade of a homogeneous MR_Grade result and remain undefined on the other seven constructors. Let \Pi_{\mathrm{App}}^{\mathcal{D}} be its domainwise extension. On the Applicable fragment, the grades recover the composed state: \Pi_{\mathrm{App}}^{\mathcal{D}} \circ T_H = \bigwedge_{J \in H} x^{(J)} = c^{\mathrm{eff}}. This is the point used by the conservative one-vector admission check.

The second object is the family of per-harbor admissions S_J(x^{(J)}). The composed vector cannot recover it because the meet retains minima and loses the contributing harbor. The holder-set economics needs that per-jurisdiction, per-counterparty information.

Both derived objects are necessary. Admissibility bits alone would discard mixed-axis provenance before w receives it. For example, tensor_meet sends a matched Applicable pair to MR_Grade and an Applicable-versus-NotApplicable pair to MR_AppVsNotApp. Both carry the Applicable grade, but their provenance differs in exactly the way Theorem 1(iii) uses.

The composed meet_result vector preserves that provenance but loses the per-harbor admission data needed by the numeric branch. The per-harbor record is the smallest argument from which both objects derive.

The third argument is an adversarial counterparty-belief model \beta, whose construction remains open. Under heterogeneous beliefs, the clearing price is a functional of the cross-counterparty belief distribution, not the objective price. The belief-layer section states the unresolved sub-obligation.

Admissibility affects price through the computed holder set. Following Definition 4.6, fix a population \mathcal{N} of candidate counterparties. Define the eligible holder set E_H(x) \subseteq \mathcal{N}, the companion’s \mathrm{Hold}_t(A) expressed as a function of the issuer’s record. It contains counterparties e whose transfers pass every required domain on both sides. The issuer’s side uses per-harbor admission, evaluating each S_J at x^{(J)}. The counterparty’s side uses e’s own record. The corridor joining e’s jurisdictions to H must also admit the transfer. Two named assumptions connect E_H to price.

A1 (Monotone eligibility). Every membership condition of Definition 4.6 is monotone in the issuer’s record, and, holding the candidate population and the corridor structure fixed, extending the harbor set adds membership conditions and removes none. Consequently E_H(x) \subseteq E_H(x') whenever x \le x' pointwise, and E_{H'}(x) \subseteq E_H(x|_H) whenever H \subseteq H'. A1 follows from the surfaces’ up-set property for verdict conditions. It remains an assumption for Definition 4.6’s corridor-admission condition.

A2 (Priced liquidity channel). At fixed cash flows and fixed beliefs, the admissible price is non-decreasing in the eligible holder set under inclusion. A2 uses the liquidity direction from Amihud and Mendelson [1] and Pástor and Stambaugh [2]. Duffie, Gârleanu, and Pedersen [3] provide the search-theoretic micro-foundation. Merton [4] and Errunza and Losq [5] derive the restricted-investor-base channel in equilibrium. Longstaff [6] bounds the discount for a marketability restriction of known horizon. The Positioning section develops these results and separates their contribution from the typed construction here.

Together, A1 and A2 connect a change in regulatory standing to a change in admissible price. The cited literature supplies the direction. The typed construction specifies the holder set, the mechanized object from which it is computed, and the conditions under which the numeric branch can run.

An obstructed compliance result returns a typed obstruction. This paper constructs the obstruction type by carrying composition’s obstruction structure into the price layer. It has four constructors:

\mathrm{PriceObstruction} \;=\; \mathbf{MixedAxisAtPricing}(o) \;\mid\; \mathbf{CannotLiftOutOfScopeToPrice} \;\mid\; \mathbf{InadmissibleNoPrice} \;\mid\; \mathbf{SanctionsTerminalNoPrice}.

\mathbf{MixedAxisAtPricing}(o) retains every required domain on which applicability disagrees across harbors. Its payload is o = (T_H(x)_d)_{d \in M} for the non-empty set M of those domains. Each entry is one of the four mixed-axis provenance classes. The map emits no price and preserves all obstructed domains together, allowing the clearing layer to refer the claim to a corridor or rule-layer authority.

\mathbf{CannotLiftOutOfScopeToPrice} covers homogeneous out-of-scope composition on a required domain. Either no harbor applies the domain (MR_NotApp), every harbor exempts it (MR_Exempt), or no harbor is present and no jurisdiction is answerable (MR_Empty). A fresh in-scope attestation from a named authority would supply a grade.

MR_NotAppVsExempt also lacks a grade, but records disagreement about the basis of exclusion. One harbor finds the domain inapplicable and another applies an exemption. A corridor authority needs this provenance to settle scope, and there is no grade against which to compare a price. This constructor therefore joins the other three mixed constructors in \mathbf{MixedAxisAtPricing}.

\mathbf{InadmissibleNoPrice} covers an in-scope failure: every required domain composes to a grade, but the eligible holder set is empty. Because verdicts are monotone, new evidence can raise the record and reopen the numeric branch.

\mathbf{SanctionsTerminalNoPrice} is the absorbing case, distinguished from \mathbf{InadmissibleNoPrice} by mechanized terminality. Once any harbor’s record reaches sanctions bottom, sanctions_bottom_cannot_become_compliant_after_meet excludes repair through further composition. Reopening the branch requires a change to the sanctioned record itself. A sanctions-bottom claim returns a typed absence of admissible price, not a zero.

The branches of w have one total order, so every input reaches exactly one branch.

First, the map checks the per-harbor record before inspecting composed domains. If any harbor’s sanctions coordinate is bottom, it returns \mathbf{SanctionsTerminalNoPrice} regardless of the other results. Terminality gives this check precedence. Resolving mixed applicability or adding an in-scope attestation leaves the sanctioned record unchanged.

Second, the map inspects the composed vector over the claim’s required domains. Let M contain every required domain where T_H(x)_d has a mixed-axis constructor. If M is non-empty, the map returns \mathbf{MixedAxisAtPricing}(o) with o = (T_H(x)_d)_{d \in M}. Thus two domains obstructed in different provenance classes are both reported, without choosing an order between them.

If M is empty, a required domain with MR_NotApp or MR_Exempt is out of scope in every harbor. A result of MR_Empty means that no harbor is present and no jurisdiction is answerable. Any such result returns \mathbf{CannotLiftOutOfScopeToPrice}. Mixed-axis results take precedence so a domain awaiting attestation cannot mask provenance needed for routing.

Third, when every required domain has MR_Grade, the claim is in scope and the map checks the holder set. An empty E_H(x) returns \mathbf{InadmissibleNoPrice}. Otherwise, the numeric branch computes Definition 4.8’s clearing price with \mathrm{Hold}_t(A) instantiated to E_H(x). Gate constructors zero each program branch whose continuation transfers the claim outside E_H(x). The measure Q prices over E_H(x) under the model supplied by that population. A2 assumes this price is monotone in the set.

Only this last branch emits an element of \mathrm{Price}. Every other branch returns a typed obstruction. The precedence is sanctions record, composed vector with mixed results before out-of-scope results, then holder set. It ensures that \mathbf{SanctionsTerminalNoPrice}, the obstruction that further composition cannot lift, is never hidden by a repairable obstruction.

The headline theorem

Theorem 1 (Admissibility-Conditioned Pricing). Fix the PDCF input \pi and the belief input \beta; let the harbor set be non-empty; assume A1 and A2. Clauses (i) and (ii) are stated over the Applicable fragment, where every coordinate of every per-harbor record carries a grade: there every required domain composes to a homogeneous MR_Grade result (tensor_meet_all_applicable_fragment, non-empty list), so no mixed-axis or out-of-scope obstruction arises and w is decided by the sanctions record and the holder-set gate alone. Clause (iii) is stated over the whole meet_result state space, because the mixed-axis results on which it has content lie outside the fragment.

(i) Monotone in the compliance state. Fix the harbor set H and the candidate population. If x \le x' pointwise in the per-harbor state order, then E_H(x) \subseteq E_H(x'), and if w emits a price at x it emits a price at x', with w(\pi, x, \beta) \;\le\; w(\pi, x', \beta). A more compliant entity issues to a weakly larger set of lawful holders at a weakly higher admissible price.

(ii) Antitone in the harbor set, through the admissibility channel. Fix a per-harbor record x over H', the candidate population, and the corridor structure. For non-empty H \subseteq H', E_{H'}(x) \subseteq E_H(x|_H), and if w emits a price over H' it emits one over H, with w(\pi, x, \beta) \;\le\; w(\pi, x|_H, \beta). An added harbor adds issuer-side requirements and removes none; the holder population it newly reaches is held fixed, and this clause does not bound that channel.

(iii) Obstruction-Faithfulness. Over the whole meet_result state space. w is total, with its branches declared in one order — the sanctions record, then the composed vector over the required domains, then the holder set — and a declared case for each of the eight meet_result constructors on every required domain. If any required domain composes to one of the four mixed-axis constructors, w returns a \mathrm{PriceObstruction} and never an element of \mathrm{Price}: \mathbf{SanctionsTerminalNoPrice} when some harbor’s record stands at the sanctions bottom, and otherwise \mathbf{MixedAxisAtPricing} carrying, for every required domain that composed to a mixed-axis constructor, that constructor and its provenance class. The numeric branch is reachable only when no harbor’s record stands at the sanctions bottom, every required domain composes to a homogeneous MR_Grade result, and the eligible holder set is non-empty.

Scope. Clauses (i) and (ii) hold on the Applicable fragment under A1–A2; clause (iii) holds on the whole composed state space and uses neither assumption. Clause (ii) bounds one of the two channels a harbor addition opens — the admissibility channel — and holds the other, the added jurisdiction’s holder population and the corridors that reach it, fixed. The two channels carry opposite signs, so the net price effect of a harbor addition is not determined by this theorem; it is recorded open below, with the mixed-axis price map and the belief layer (O-14, the obligation ledger entry below).

Proof. (i) On the Applicable fragment, every coordinate of every record is an Applicable grade. Each required domain therefore composes to MR_Grade of the per-harbor meet (tensor_meet_all_applicable_fragment, non-empty list). The sanctions record and holder-set gate determine w.

Each surface is monotone in the state order: its admitted set is an up-set by the companion’s definition. Thus every required verdict of Definition 4.6 is preserved as the record rises, and A1 gives E_H(x) \subseteq E_H(x'). The numeric branch is preserved upward. A sanctions coordinate above bottom at x remains above bottom at x' \ge x. Also, E_H(x')\supseteq E_H(x) is non-empty whenever E_H(x) is. On that branch, A2 gives w(\pi, x, \beta) \le w(\pi, x', \beta).

(ii) For H \subseteq H', membership in E_{H'}(x) requires every condition for membership in E_H(x|_H) plus the added harbors’ verdicts. With the population and corridor structure fixed, A1 gives E_{H'}(x) \subseteq E_H(x|_H). Restricting the harbor set can only remove a sanctions bottom and enlarge the eligible set, preserving the numeric branch as in (i). A2 then gives the inequality in the opposite direction.

Both clauses use exactly the two named economic assumptions, and only for their directions. The companion’s definition and multi-harbor proposition fix the surface orientations, while the mechanized composition theorem supplies the fragment routing. The inequalities are paper theorems over that core under A1–A2. They are not mechanized results.

(iii) The sanctions check is a decidable predicate on the per-harbor record and determines w first. At sanctions bottom, it returns \mathbf{SanctionsTerminalNoPrice} before inspecting any domain.

After that check, each required domain ranges over meet_result, with exactly eight constructors. The branch declaration covers each constructor in a fixed order: mixed-axis results, out-of-scope results, then the two MR_Grade sub-cases. This count and order make the analysis exhaustive.

The four mixed constructors return \mathbf{MixedAxisAtPricing} with provenance from every required domain where they occur. Once no required domain is mixed, MR_NotApp, MR_Exempt and MR_Empty return \mathbf{CannotLiftOutOfScopeToPrice}. When every required domain has MR_Grade, an empty eligible set returns \mathbf{InadmissibleNoPrice}, and a non-empty set reaches the numeric branch.

The reason for withholding a number from the four mixed constructors concerns the pricing channel. The numeric branch depends on the eligible holder set, whose membership requires verdicts. A mixed-axis result supplies no verdict. For example, MR_AppVsNotApp records an in-scope grade from one harbor and an out-of-scope finding from another, without partitioning the harbor set.

Determining eligibility would require which harbors’ scope governs the transfer and the sizes of the affected holder populations. This is the second channel in the harbor-addition section below. Compare a price on MR_AppVsNotApp with the fragment price at the same grade. Their difference is the net effect of adding a harbor that excludes the domain. That effect remains open. The argument also applies to MR_AppVsExempt and MR_AppVsNotAppVsExempt, which carry grades.

MR_NotAppVsExempt carries no grade. No harbor graded the domain, so there is no Applicable-fragment price for comparison. The harbors also disagree about the governing exclusion: inapplicability in one and an exemption in another. A corridor authority must settle that issue before scope and the holder set are fixed.

A total numeric branch on the four mixed constructors would therefore not be a function of the inputs supplied to w. On the three graded constructors, it would resolve the unknown harbor-addition sign. On the fourth, it would price a domain that no harbor graded. The typed obstruction retains these unresolved cases.

The supporting mechanized impossibility concerns value-level composition. Its full-strength form is heyting_closure_impossible_with_audit_fix (Qed, LatticeOrthogonalFull.v). It ranges over every commutative, associative, idempotent total operation on the five-state cell that extends the grade meet. No such operation preserves both the compliance signal and NotApplicable’s orthogonality. Thus every semilattice extension, not only the selected meet, loses an axis when it collapses mixed input to one state.

The value-layer companion in TensorAlignment.v, no_total_tensor_factor_meet_preserves_signal_and_orthogonality (Qed), establishes a narrower dichotomy. Its hypotheses preserves_app_signal_on_notapp and keeps_notapp_orthogonal_to_app are jointly unsatisfiable. The first requires Applicable output on an Applicable-versus-NotApplicable input, and the second forbids it. This two-line result records the incompatibility of the two requirements for a total tensor_factor-valued meet. Together, the results motivate the structured meet_result type rather than a fourth tensor factor.

Both theorems quantify over value-level operators. Neither alone prohibits a numeric price on mixed input. That requires the price-layer argument above. No single Coq constructor discharges (iii). The mechanized content comprises the impossibility, the mixed-result family, and tensor_meet_all_flags_exact, which preserves the exact input provenance. \square

The monotonicity clauses depend on the companion’s orientations and A1–A2. Obstruction-faithfulness follows from the declared routing, exhaustively by constructor count and precedence. The price-layer argument explains that choice. Mixed results leave the holder-set gate without a verdict. A numeric branch would resolve an open harbor effect or price an ungraded domain.

There is no mechanized pricing operator. The mechanized results establish the meet, exact provenance, and impossibility, both for every semilattice extension of the grade meet and for the value-layer dichotomy.

The obligation ledger entry

O-14 in the programme’s proof-obligation ledger records the remaining construction and links it to O-6, the underlying mixed-axis MeetResult formalization. Its target is a total price map over the whole TensorValue space. Theorem 1 partially discharges that target on the Applicable fragment under A1–A2. The ledger gives a closure route and keeps the belief layer and net effect of a harbor addition explicitly open.

The ledger’s closure route has three parts. First, lift tensor_meet_all to a PriceObstruction-valued price reduction over a concrete audit bundle. Second, mechanize A1’s eligibility monotonicity over the full state space. It is currently paper-proved for verdict conditions and assumed for the corridor condition. Third, formalize \beta as the latent quantity over the joint distribution of intrinsic PDCF, composed tensor, and counterparty beliefs. Prove a bias or identifiability bound under belief deviation.

The belief portion inherits O-6’s mixed-axis impossibility. A price map that ignores composition obstructions cannot be faithful, so the belief formalization must build on obstruction-faithfulness.

The open sign of a harbor addition

Adding a harbor creates two price effects. The entity becomes answerable to another regulator, which can only narrow its composed admissibility surface. It also becomes issuable into another jurisdiction’s investor population, which can only widen the population of possible holders. Theorem 1(ii) bounds the first effect while holding the second fixed.

This paper gives no bound on the holder-population effect, which need not be smaller. Its size depends on the added jurisdiction’s investor population and the carried state that its corridor permits local holders to rely on. It also depends on how strongly the added harbor’s grades constrain the domains required to hold the instrument. Composition fixes none of these inputs, and two are empirical.

The net sign is therefore unknown. Composition alone cannot decide whether an entity should add a harbor. Answering that question requires a model of holder population as a function of the harbor set, separate from the compliance lattice. Neither this paper nor its companions develops that model.

The open belief layer

The adversarial counterparty-belief layer remains open. It concerns the joint distribution of intrinsic PDCF, the composed compliance tensor, and the counterparty-belief model. Theorem 1 holds \beta fixed and establishes no price response to changes in the cross-counterparty belief distribution.

This is an identification problem. Under heterogeneous beliefs, the clearing price is a functional of a counterparty-belief distribution that is not directly observed. Manski’s partial-identification framework [7] applies: such a functional lacks point identification without additional assumptions, and those assumptions are part of the problem. The target is a bounded identified set rather than a point.

Closing this obligation requires a latent-quantity formalization, a stated identification assumption, and a proved bias or identifiability bound. The price under adversarial beliefs remains open until those are supplied.

Positioning

The related work in Intelligent Assets covers institutional economics, smart-contract verification, programmable-securities standards (ERC-1400, ERC-1404, ERC-3643), and legal theory. It takes no result from asset pricing. Definition 4.8 lets the holder set enter price both through gates that zero inadmissible transfers and through the population used by the pricing measure. It leaves that measure to an unconstructed model of how the population prices.

The companion therefore states dependence without determining its direction. This paper uses asset-pricing results to connect a tighter admissibility filter to a lower price.

Two equilibrium results establish the holder-base channel. Merton [4] prices assets held only by investors who know them. His shadow-cost premium falls as the investor base widens, so price rises with the holder set at fixed cash flows. Errunza and Losq [5] obtain the channel under legal restrictions: securities barred to one investor class carry a super risk premium. A compliance-admissible set is their restricted investor base, with the restriction computed by mechanized composition.

Longstaff [6] supplies a quantitative bound alongside A2’s direction. When the restriction is a pure holding bar of known horizon, its discount is at most the value of a lookback option over that horizon.

Duffie, Gârleanu, and Pedersen [3] price over-the-counter assets under search frictions. Both price level and bid-ask spread reflect the difficulty of finding counterparties and the bargaining division of gains. The compliance filter restricts the matching set: admissible holders form a search-feasible set. A tighter filter therefore creates a thinner market and a larger discount.

Their model supplies the micro-foundation. This paper’s typed conditioning identifies the set over which matching occurs. Theorem 1 establishes that under A1–A2, tightening the filter cannot raise the cleared price above the looser-filter price.

Amihud and Mendelson [1] establish that illiquidity is priced cross-sectionally: assets with higher bid-ask spreads earn higher gross returns. Pástor and Stambaugh [2] establish that aggregate liquidity is a priced risk factor. These results support the monotone direction. A narrower holder set reduces liquidity, which commands a premium and raises required return. At fixed cash flows, this lowers price, so the screened instrument prices weakly below the unscreened one. A2 uses that direction without re-estimating the empirics or proposing a competing factor.

CPSS-IOSCO PFMI Principle 8 (settlement finality) [8] supplies the standard for the clearing layer’s settlement guarantee. Intelligent Assets states the cross-zone commit and finality-certificate assumptions without naming that Principle. This paper cites it directly. An admissible price presupposes settlement finality under Principle 8. The credit-and-liquidity-risk principles governing the clearing counterparty’s own resources address a separate requirement.

The contribution uses these established models and channels to condition price on a mechanized compliance filter. It states the two economic steps as assumptions and represents composition obstructions as price-layer objects. In particular, disagreement about applicability across harbors retains its provenance instead of silently becoming a number. That composition has no representation in the cited pricing literature.

What is proved and what is open

Mechanized, unconditional: the Applicable-fragment grade-meet laws and the n-ary composition core (TensorAlignment.v, 43 Qed); the mixed-axis provenance constructors, their exactness, and the value-layer dichotomy in the same file; the full-strength mixed-axis impossibility over every semilattice extension of the grade meet (LatticeOrthogonalFull.v, heyting_closure_impossible_with_audit_fix, 29 Qed, 0 Admitted, 0 Axiom); sanctions terminality at the value layer (ComplianceContext.v, sanctions_bottom_cannot_become_compliant_after_meet, Qed, 0 axioms).

Mechanized, parametric: op verdict preservation (CompilationSoundness.v, verdict_preservation_sanctions, Qed, parametric over the abstract host primitive host_sanctions).

Paper-proved over the mechanized meet: monotonicity of the admissibility surface S_J in the state order and antitonicity of S_H in the harbor order (both established in the composing-compliance companion, the first as the definition of the surface, the second as its multi-harbor proposition); Theorem 1(iii) obstruction-faithfulness over the whole composed state space, exhaustive in one declared order over the sanctions record, the eight meet_result constructors on every required domain, and the two MR_Grade sub-cases, definitional in the routing, and forced at the price layer by the open sign of a harbor addition. Under A1–A2 in addition: Theorem 1(i) and 1(ii) on the Applicable fragment.

Assumed, with named support: A1, monotone eligibility — the up-set property of Definition 4.6’s verdict conditions, assumed on its corridor condition; A2, the priced liquidity channel — Amihud–Mendelson [1], Pástor–Stambaugh [2], Duffie–Gârleanu–Pedersen [3], Merton [4], Errunza–Losq [5], with Longstaff [6] bounding the discount where the restriction is a holding bar — imported for direction, not re-derived.

Open, not claimed: the mixed-axis price map over the full tensor state space (O-14); the adversarial belief layer (the belief portion of O-14, inheriting the mixed-axis impossibility of O-6); the net price effect of a harbor addition, where the admissibility channel bounded by Theorem 1(ii) and the holder-population channel it holds fixed carry opposite signs and the second is unmodelled.

The settlement-finality boundary rests on CPSS-IOSCO PFMI Principle 8 [8], the standard the clearing layer targets.

A claim issued by a multi-harbored entity therefore prices subject to an admissibility filter. On the fragment with mechanized compliance composition, two named economic assumptions make price monotone in compliance state and antitone in the harbor set. On the whole composed space, the construction preserves composition obstructions. The full-state-space price map, adversarial belief distribution, and net sign of a harbor addition remain explicit ledger obligations.

References

1. Amihud, Y. and Mendelson, H. (1986). Asset pricing and the bid-ask spread. Journal of Financial Economics, 17(2), pp. 223-249.
2. Pástor, Ľ. and Stambaugh, R. F. (2003). Liquidity risk and expected stock returns. Journal of Political Economy, 111(3), pp. 642-685.
3. Duffie, D., Gârleanu, N. and Pedersen, L. H. (2005). Over-the-counter markets. Econometrica, 73(6), pp. 1815-1847.
4. Merton, R. C. (1987). A simple model of capital market equilibrium with incomplete information. Journal of Finance, 42(3), pp. 483-510.
5. Errunza, V. and Losq, E. (1985). International asset pricing under mild segmentation: theory and test. Journal of Finance, 40(1), pp. 105-124.
6. Longstaff, F. A. (1995). How much can marketability affect security values? Journal of Finance, 50(5), pp. 1767-1774.
7. Manski, C. F. (2003). Partial Identification of Probability Distributions. Springer Series in Statistics. Springer. See also Manski, C. F. (2004), Measuring expectations, Econometrica, 72(5), pp. 1329-1376.
8. Committee on Payment and Settlement Systems and Technical Committee of the International Organization of Securities Commissions (2012). Principles for Financial Market Infrastructures, Principle 8 (Settlement finality). Bank for International Settlements.