What ships as law

Three things are settled before this paper begins, and the price map is built on top of them.

The first is the admissibility filter. The companion Composing Compliance Across Jurisdictions establishes that on the Applicable fragment the per-domain factor is a finite distributive lattice, the product over the tensor’s 23 compliance domains — the Applicable-fragment lattice \mathcal{L}_{23} — is again finite distributive, and the multi-harbor compliance state is the pointwise meet across harbors. Write S_J for the admissibility surface of jurisdiction J: it maps a compliance state c \in \mathcal{L}_{23} to an admissibility verdict in \{0 < 1\}. Two orders act on the surfaces, and they enter the price with opposite signs.

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 is the companion’s definition of the admissibility surface, and the orientation is fixed there, not chosen here.

In the harbor order, composition is antitone. For a harbor set H, the composed surface is S_H = \min_{J \in H} S_J — admitted exactly when every harbor admits — so H \subseteq H' gives S_{H'} \le S_H pointwise. Each additional harbor can only shrink the admitted set. This is the companion’s multi-harbor proposition. Becoming more compliant widens the set of lawful holders; becoming answerable to more jurisdictions narrows it.

The two orders act on two different evaluation points, and the companion keeps them apart. An entity holds one state per harbor — write x^{(J)} for its state in harbor J — and the composed state c^{\mathrm{eff}} = \bigwedge_{J \in H} x^{(J)} is their pointwise meet. Admission is per-harbor, each surface at its own state. Evaluating every surface at the single point c^{\mathrm{eff}} instead is conservative: c^{\mathrm{eff}} \le x^{(J)} and admitted sets are up-sets, so if every surface passes at the composed point then every harbor passes its own state, and the converse fails (the companion’s composed-check corollary). Where the two evaluations differ, per-harbor admission is the admission; the composed-point check is its sound approximation.

The second is the mechanized core. The grade-meet laws, the n-ary composition operator, and the mixed-axis impossibility are mechanized in Coq in TensorAlignment.v (43 Qed, 0 Admitted, 0 Axiom). The binary meet on tensor factors is tensor_meet; the composition operator on the full tensor state space is its n-ary form tensor_meet_all; on a non-empty all-Applicable input it agrees with the Applicable-fragment meet (tensor_meet_all_applicable_fragment), and on mixed inputs it returns a structured meet_result that flags exactly which applicability axes appeared (tensor_meet_all_flags_exact). The structured outcome has constructors MR_Grade, MR_NotApp, MR_Exempt, MR_AppVsNotApp, MR_AppVsExempt, MR_NotAppVsExempt, MR_AppVsNotAppVsExempt, MR_Empty. The four mixed-axis constructors carry the provenance of a composition where applicability disagreed across jurisdictions. The reason such a result cannot be collapsed to a single grade without losing the compliance signal is itself a theorem, mechanized at full strength in LatticeOrthogonalFull.v, a standalone Coq artifact of the same programme (29 Qed, 0 Admitted, 0 Axiom): heyting_closure_impossible_with_audit_fix proves that no total operation on the five-state cell — Applicable at one of three grades, NotApplicable, Exempt — that is commutative, associative, and idempotent and extends the grade meet on Applicable inputs can both keep the Applicable compliance signal against a NotApplicable counterpart (Compliant composed with NotApplicable is not NotApplicable) and keep NotApplicable orthogonal to the Applicable grades (NotApplicable composed with a grade is neither that grade nor Exempt). Every semilattice extension of the grade meet loses one axis, so a structured result is forced, not chosen. TensorAlignment.v carries the value-layer companion, no_total_tensor_factor_meet_preserves_signal_and_orthogonality: no total operator on the tensor factor both preserves the Applicable compliance signal against a NotApplicable counterpart and keeps NotApplicable orthogonal to the Applicable grades.

The third is sanctions terminality. A sanctions-bottom result is absorbing and cannot be undone by composition: ComplianceContext.v, in the Op development, proves sanctions_bottom_cannot_become_compliant_after_meet (36 Qed, 0 Admitted, 0 Axiom, 0 Parameter — unconditional). A related verdict-preservation result, verdict_preservation_sanctions in CompilationSoundness.v, is Qed-closed but parametric over the abstract host primitive host_sanctions; label it Qed-closed-modulo-abstract-host.

One boundary on this section, and one disambiguation. Both orientations — monotonicity of S_J in the state order, and antitonicity of S_H in the harbor order — come from Composing Compliance Across Jurisdictions, where the admissibility surface is defined (as a monotone map whose admitted set is an up-set) and where the multi-harbor proposition establishes S_H=\min_{J\in H}S_J. The shorter note that circulates under the title How Compliance Composes carries the lattice construction and the mixed-axis dichotomy, citing the same Coq artifacts; it defines no admissibility surface, so it is not the citation target for either orientation. Neither orientation is a theorem in either .v file: the Coq development carries the grade-meet laws, the n-ary composition, and the impossibility, not a threshold-surface theorem. Where this paper uses either orientation, the status is “paper-proved over the mechanized meet,” and that label is carried through to the theorem below.

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},

where \mathcal{D} is the domain index of the tensor and \mathrm{TF} is the tensor-factor type of the mechanized core: on each domain, an Applicable grade, NotApplicable, or Exempt.

The first argument is the intrinsic present-discounted cash flow of the instrument: the \Phi-valuation of the claim program in the sense of the Intelligent Assets paper, the source from which face value, coupon schedule, default waterfall, and the risk-neutral expectation derive. This is standard and not the contribution.

The second argument is the entity’s compliance record as mechanized law carries it: one tensor-factor vector per harbor, x = (x^{(J)})_{J \in H}, with x^{(J)}_d the entity’s factor on domain d as attested in harbor J. On the Applicable fragment, where every coordinate carries a grade, x^{(J)} is a point of \mathcal{L}_{23}. The compliance input is fixed by construction to be the attested record, never a free compliance state that a caller could supply unfiltered.

Two objects derive from the record, and the price map uses both. The first is the composed vector T_H(x) \in \mathrm{MeetResult}^{\mathcal{D}}: on each domain d, T_H(x)_d is tensor_meet_all applied to the per-harbor factors (x^{(J)}_d)_{J \in H}, an element of the eight-constructor meet_result type. This is the routing datum: it detects mixed applicability, uniformly out-of-scope domains, and the empty harbor set, and on a homogeneous in-scope domain it carries the composed grade. Let \Pi_{\mathrm{App}} read a homogeneous MR_Grade result and return its grade, undefined on the other seven constructors, and let \Pi_{\mathrm{App}}^{\mathcal{D}} be its domainwise extension; on the Applicable fragment the composed grades are exactly the composed state, \Pi_{\mathrm{App}}^{\mathcal{D}} \circ T_H = \bigwedge_{J \in H} x^{(J)} = c^{\mathrm{eff}}, so the meet computes the point at which the conservative one-vector admission check runs. The second derived object is the family of per-harbor admissions S_J(x^{(J)}), which the composed vector cannot supply: the meet takes the minimum across harbors and forgets which harbor contributed what, and the holder-set economics below is per-counterparty and per-jurisdiction.

This fixes the type of the compliance argument from both sides. A vector of admissibility bits would have destroyed the mixed-axis provenance before w was ever called: tensor_meet sends a matched Applicable pair to MR_Grade and an Applicable-versus-NotApplicable pair to MR_AppVsNotApp, carrying the Applicable grade in both cases, and the two compositions differ in exactly the provenance that clause (iii) of Theorem 1 turns on. The composed meet_result vector alone would have preserved that provenance and destroyed the per-harbor admission data the numeric branch consumes. The per-harbor record is the smallest argument from which both derive.

The third argument is an adversarial counterparty-belief model \beta. It is open. The price a claim clears at under heterogeneous beliefs is a functional of the cross-counterparty belief distribution, not the objective price. This is the open sub-obligation carried in the belief-layer section below and is not discharged here.

Admissibility prices through the holder set, and the holder set is computed, not declared. Following the companion’s Definition 4.6, fix a population \mathcal{N} of candidate counterparties and let the eligible holder set E_H(x) \subseteq \mathcal{N} — the companion’s \mathrm{Hold}_t(A), written as a function of the issuer’s record — be the set of counterparties e whose transfer has a passing verdict on every domain the transfer requires, on both sides — on the issuer’s side per-harbor admission, each S_J evaluated at x^{(J)}; on the counterparty’s side e’s own record — and whose corridor joining e’s jurisdictions to H admits the transfer. Two named assumptions carry E_H to a price, and the theorem is stated under them.

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'. On the verdict conditions A1 is the up-set property of the surfaces and costs nothing; it is an assumption where the corridor-admission condition of Definition 4.6 enters.

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 imports its direction from the asset-pricing literature and adds nothing to it. Amihud and Mendelson [1] show that illiquidity is priced: assets with higher bid-ask spreads earn higher gross returns, so a narrower holder set raises required return and lowers price at fixed cash flows. Pástor and Stambaugh [2] show that aggregate liquidity is a priced state variable. Duffie, Gârleanu, and Pedersen [3] give the search-theoretic micro-foundation: in over-the-counter markets, prices and bid-ask spreads are determined by search frictions and bargaining power, and tighter restrictions on who may hold an instrument map directly to thinner matching and a larger discount. Merton [4] and Errunza and Losq [5] derive the channel itself in equilibrium — a bounded investor base carries a shadow-cost premium that falls as the base widens, and a legally segmented one a super risk premium — which is the direct prior art for a compliance-restricted holder set. Longstaff [6] bounds the size of the effect: a marketability restriction of known horizon discounts the instrument by at most the value of a lookback option over that horizon.

The composite — admissibility into holder set (A1), holder set into price (A2) — is what carries a change in regulatory standing to a change in admissible price. Its direction comes from the literature above. What this paper adds is the typed conditioning: which holder set, computed from which mechanized object, gated by which branch discipline.

The price map never silently coerces an obstructed compliance result into a number. The obstruction type is this paper’s construction, the price-layer lift of the composition’s obstruction structure, with four constructors:

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

\mathbf{MixedAxisAtPricing}(o) carries the mixed-axis composition results on every required domain where applicability disagreed across the entity’s harbors: o = (T_H(x)_d)_{d \in M} for the non-empty set M of such domains, each entry one of the four mixed-axis provenance classes. No price is emitted; the provenance is preserved, on every obstructed domain at once, so the clearing layer can route the claim to a corridor or rule-layer authority rather than guess a number. \mathbf{CannotLiftOutOfScopeToPrice} is the price-layer image of a homogeneous out-of-scope composition on a required domain — every harbor excludes the domain on the same ground, the domain governing the entity in no harbor (MR_NotApp) or an exemption in force everywhere (MR_Exempt), or the harbor set is empty and no jurisdiction is answerable (MR_Empty) — and a fresh in-scope attestation from a named authority is what would supply a grade. MR_NotAppVsExempt also carries no grade, and is not of this kind: its harbors disagree over which exclusion governs — the domain not governing the entity in one harbor, an exemption in force in another — and that disagreement is provenance a corridor authority needs before the domain’s scope is settled, with no comparison grade to price against, so it routes with the other three mixed constructors to \mathbf{MixedAxisAtPricing}. \mathbf{InadmissibleNoPrice} is the in-scope failure: every required domain composes to a grade and the eligible holder set is empty. It is repairable — verdicts are monotone, so new evidence raises the record and can reopen the numeric branch. \mathbf{SanctionsTerminalNoPrice} is the absorbing case of inadmissibility, distinguished from \mathbf{InadmissibleNoPrice} by the mechanized terminality theorem: once any harbor’s record stands at the sanctions bottom, sanctions_bottom_cannot_become_compliant_after_meet forecloses repair by further composition, and only a change to the sanctioned record itself reopens the branch. A sanctions-bottom claim has no admissible price, and the absence is typed, not a zero.

The branches of w are declared in one total order, and every input reaches exactly one of them. First the record, before any domain is inspected: if the sanctions coordinate of any harbor’s record stands at the bottom of its chain, the branch is \mathbf{SanctionsTerminalNoPrice}, whatever the other domains compose to. The check reads the per-harbor record directly, and it comes first because the terminality theorem makes it the one obstruction no later branch could lift: an authority’s elimination of a mixed-axis result or a fresh attestation on an out-of-scope domain leaves the sanctioned record where it stands. Second the composed vector, over the domains the claim requires. Let M be the set of required domains on which T_H(x)_d is one of the four mixed-axis constructors; if M is non-empty the branch is \mathbf{MixedAxisAtPricing}(o) with o = (T_H(x)_d)_{d \in M}, so two required domains obstructed in different provenance classes are both reported and no order between domains has to be chosen. If M is empty and some required domain composes to MR_NotApp or MR_Exempt — the domain is out of scope in every harbor — or to MR_Empty — the harbor set is empty and no jurisdiction is answerable — the branch is \mathbf{CannotLiftOutOfScopeToPrice}; the mixed-axis family is taken before the out-of-scope domains so that a provenance the clearing layer must route on is never masked by a domain that awaits attestation. Third the holder set: when every required domain composes to MR_Grade the claim is in scope, and the filter applies through the holder set. If E_H(x) is empty, the branch is \mathbf{InadmissibleNoPrice}; otherwise the numeric branch runs, and the price is the clearing price of Definition 4.8 with \mathrm{Hold}_t(A) instantiated to E_H(x): the gate constructors zero every branch of the claim program whose continuation transfers the claim to a counterparty outside E_H(x), and Q prices over the population E_H(x), under the pricing model that population supplies — A2 is the assumption that this price is monotone in the set. The map emits an element of \mathrm{Price} only on that last branch; otherwise it returns a typed obstruction, and where an input carries more than one, the order above decides which — the sanctions record before the composed vector, the mixed-axis family before the out-of-scope domains, the composed vector before the holder set — so that \mathbf{SanctionsTerminalNoPrice}, the one of the four that no further composition can lift, is never hidden behind an obstruction that could be.

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, so each required domain composes to MR_Grade of the meet of the per-harbor grades (tensor_meet_all_applicable_fragment, non-empty list), and w is decided by the sanctions record and the holder-set gate. Each surface is monotone in the state order (the companion’s definition: the admitted set is an up-set), so 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 stays above bottom at x' \ge x, and E_H(x')\supseteq E_H(x) is non-empty whenever E_H(x) is. On the numeric branch A2 turns the inclusion into w(\pi, x, \beta) \le w(\pi, x', \beta).

(ii) For H \subseteq H', membership in E_{H'}(x) requires every condition membership in E_H(x|_H) requires, together with the added harbors’ verdicts; with the population and corridor structure fixed, A1 gives E_{H'}(x) \subseteq E_H(x|_H). Branch preservation runs as in (i) — restricting the harbor set can only remove a sanctions bottom and can only grow the eligible set — and A2 applies in the opposite direction.

The non-formal ingredients of both clauses are exactly the two named assumptions, imported for their directions only; the orientations of the surfaces are fixed by the companion’s definition and its multi-harbor proposition, and the fragment routing is the mechanized composition theorem. Both inequalities are therefore paper theorems over the mechanized core under A1–A2, not mechanized results.

(iii) The sanctions check is a decidable predicate on the per-harbor record, and w is decided by it first: at the sanctions bottom the branch is \mathbf{SanctionsTerminalNoPrice} before any domain is inspected. Past it, on each required domain the composed argument ranges over meet_result, which has exactly eight constructors, and the branch declaration gives one case for each, in a fixed order over the required domains — the mixed-axis family, then the out-of-scope constructors, then the two MR_Grade sub-cases — so the analysis is exhaustive by the constructor count and the declared order. The four mixed-axis constructors take \mathbf{MixedAxisAtPricing} carrying their provenance on every required domain where they appear; MR_NotApp, MR_Exempt and MR_Empty take \mathbf{CannotLiftOutOfScopeToPrice} once no required domain is mixed; MR_Grade on every required domain takes \mathbf{InadmissibleNoPrice} on an empty eligible set and the numeric branch otherwise.

Why the mixed four may not be given a number is a statement about the pricing channel, not about the meet. The numeric branch is a function of the eligible holder set, and membership in that set is decided by required verdicts. On a mixed-axis result there is no verdict to decide with: MR_AppVsNotApp records that some harbor found the domain in scope with the carried grade and some other harbor found it out of scope, and the composed value names no partition of the harbor set. Deciding eligibility anyway would require the further datum of which harbors’ scoping governs the transfer and how large the affected holder populations are. That datum is exactly the second channel of the harbor-addition section below, the one this paper declines to sign: the difference between a price on MR_AppVsNotApp and the Applicable-fragment price at the same carried grade is the net effect of adding a harbor that does not apply the domain, and that net effect is recorded as open. The same argument covers MR_AppVsExempt and MR_AppVsNotAppVsExempt, each of which carries a grade. MR_NotAppVsExempt carries none and refuses on its own terms: no harbor graded the domain, so there is no Applicable-fragment price to compare against, and the harbors disagree over which exclusion governs — the domain not governing the entity in one harbor, an exemption in force in another — which is the datum a corridor authority settles before the domain’s scope, and with it any holder set, is fixed. A total numeric branch on the mixed four would therefore not be a function of the inputs w receives: on the three graded constructors it would silently resolve a sign this paper states it does not know, and on the fourth it would price a domain no harbor has graded. The typed obstruction is the alternative to resolving either.

The mechanized impossibility sits below this argument, and this paper claims of it exactly what it proves. At full strength it is heyting_closure_impossible_with_audit_fix (Qed, LatticeOrthogonalFull.v): over every commutative, associative, idempotent total operation on the five-state cell that extends the grade meet, the compliance signal and the orthogonality of NotApplicable cannot both survive, so no semilattice extension of the grade meet — not only the meet the development chose — carries a mixed-axis input to a single state without losing an axis. Its value-layer companion in TensorAlignment.v, no_total_tensor_factor_meet_preserves_signal_and_orthogonality (Qed), does less, and is read here for what it is: its two hypotheses, preserves_app_signal_on_notapp and keeps_notapp_orthogonal_to_app, are jointly unsatisfiable — the first demands an Applicable output on an Applicable-versus-NotApplicable input, the second forbids one — so it is a two-line dichotomy recording that the two desiderata for a total tensor_factor-valued meet cannot both hold. Together they are the reason meet_result exists as a structured result type rather than a fourth tensor factor. Both quantify over value-level operators, not over price maps, so neither by itself forbids a numeric price on a mixed-axis input; the price-layer reason is the one given in the paragraph above. There is no single Coq constructor discharging (iii) — the mechanized content is the impossibility, the family of mixed-axis results, and tensor_meet_all_flags_exact, which is what keeps their provenance faithful to the inputs. \square

The clauses rest on different supports: the monotonicities on the companion’s orientations plus A1–A2, faithfulness on the routing alone. Faithfulness is definitional and exhaustive by the constructor count and the declared order, and what makes the routing the right choice rather than an arbitrary one is the price-layer argument above: on a mixed-axis result the holder-set gate has no verdict to consume, and any numeric branch would decide the harbor-addition sign this paper leaves open or price a domain no harbor has graded. Neither is claimed as a mechanized pricing theorem, because no pricing operator is mechanized; what is mechanized is the meet, the provenance and its exactness, and the impossibility on which the routing is built — at full strength over every semilattice extension of the grade meet, and as the value-layer dichotomy.

The obligation ledger entry

The frontier this paper exposes is registered as O-14 in the programme’s proof-obligation ledger, cross-linked to O-6 (the mixed-axis MeetResult formalization on which it depends). The ledger entry states the full-state-space target — a total price map on the whole TensorValue space — records Theorem 1 as the partial discharge on the Applicable fragment under A1–A2, names the closure route, and marks the belief layer and the net sign of a harbor addition as explicitly open.

The closure route, stated in the ledger, has three parts. Lift tensor_meet_all to a PriceObstruction-valued price reduction over a concrete audit bundle. Mechanize A1’s eligibility monotonicity over the full state space, which is currently paper-proved on its verdict conditions and assumed on its corridor condition. Formalize \beta as the latent quantity over the joint distribution of intrinsic PDCF, composed tensor, and counterparty beliefs, and prove a bias or identifiability bound under belief deviation. The belief portion inherits the mixed-axis impossibility of O-6: a price map that ignored the obstruction structure of composition could not be faithful, so the belief-layer formalization is built on top of obstruction-faithfulness, not beside it.

The open sign of a harbor addition

Theorem 1(ii) bounds one of the two channels a harbor addition opens, and holds the other fixed. An entity that adds a harbor becomes answerable to one more regulator, which can only narrow its composed admissibility surface; it simultaneously becomes issuable into one more jurisdiction’s investor population, which can only widen the set of people who might hold what it issues.

The first channel is bounded here. The second is not, and it is not obviously smaller. Its size depends on the added jurisdiction’s investor population, on how much of the entity’s carried state the corridor into that jurisdiction lets local holders rely on, and on how binding the added harbor’s grades are in the specific domains that gate holding for the instrument in question. None of those is fixed by the composition algebra, and two of them are empirical.

The net sign of a harbor addition is therefore unknown, and this paper does not claim it. The composition algebra, read alone, appears to answer the question — should an entity add a harbor? — in the negative, and it does not. Closing it requires a model of the holder population as a function of the harbor set, which is a different object from the compliance lattice and is not developed here or in the companion papers.

The open belief layer

The adversarial counterparty-belief layer is the part of the three-input price that this paper does not close and does not claim. It is the joint distribution over intrinsic PDCF, the composed compliance tensor, and the counterparty-belief model. Theorem 1 holds the belief input \beta fixed; it says nothing about how price moves as the cross-counterparty belief distribution moves.

The obstruction is an identification problem, not an engineering gap. The price a claim clears at under heterogeneous beliefs is a functional of the distribution of counterparty beliefs, and that distribution is not directly observed. Manski’s work on partial identification [7] is the precise frame: when the object of interest is a functional of an unobserved belief distribution, point identification fails without assumptions that are themselves the content of the problem, and the target is a bounded identified set rather than a point. The price under adversarial beliefs is exactly such a functional. Until it is formalized — as a latent quantity with a stated identification assumption and a proved bias or identifiability bound — it remains an open obligation, and this paper carries the obligation statement, not a closure.

Positioning

The Intelligent Assets paper’s related-work section engages institutional economics, smart-contract verification, programmable-securities standards (ERC-1400, ERC-1404, ERC-3643), and legal theory, and takes no result from the asset-pricing literature. Its Definition 4.8 lets the admissible holder set enter the clearing price twice — as the gate that zeroes every branch transferring the claim outside the set, and as the population over which the pricing measure prices — and then leaves that measure to an unconstructed model of how the holder population prices, so the dependence is stated there and never signed: nothing in the companion relates a tighter filter to a lower price. This paper imports the asset-pricing literature as the channel from admissibility to price.

The channel is owned by two equilibrium results. Merton [4] prices assets held only by the investors who know them and derives a shadow-cost premium that falls as the investor base widens, so price rises with the holder set at fixed cash flows. Errunza and Losq [5] derive the same channel when the restriction is legal rather than informational: securities one investor class is barred from holding carry a super risk premium. A compliance-admissible holder set is exactly their restricted investor base, with the restriction computed by mechanized composition rather than assumed. Longstaff [6] bounds the effect: the discount for a marketability restriction of known horizon is at most the value of a lookback option over that horizon, a quantitative ceiling beside A2’s sign where the restriction is a pure holding bar.

Duffie, Gârleanu, and Pedersen [3] price over-the-counter assets under search frictions: the bid-ask spread and the level both reflect how hard it is to find a counterparty and how bargaining power splits the gains from trade. The compliance filter is, in their terms, a restriction on the matching set — a compliance-admissible holder set is a search-feasible set — so a tighter filter is a thinner market and a larger discount. Their model supplies the micro-foundation; this paper supplies the typed conditioning that says which holder set the search runs over, and Theorem 1 signs it: 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; Pástor and Stambaugh [2] establish that aggregate liquidity is a priced risk factor. Together they justify the monotone direction: a more restricted holder set is less liquid, and less liquidity commands a premium, so the screened instrument prices weakly below the unscreened one at fixed cash flows. This paper does not re-estimate their empirics or propose a competing factor; it uses their established direction as A2.

CPSS-IOSCO PFMI Principle 8 (settlement finality) [8] is the standard against which the clearing layer’s settlement guarantee is evaluated. The Intelligent Assets paper carries the cross-zone commit and its finality-certificate assumptions without naming the Principle; this paper names it and cites it directly. A price is admissible only against a settlement that achieves finality under Principle 8, so the price map presupposes the finality boundary. The relevant principle is finality, distinct from the credit-and-liquidity-risk principles that govern the clearing counterparty’s own resources.

The contribution against this prior art is not a new pricing model and not a new channel. It is the typed conditioning of price on a mechanized compliance filter, with the channel’s two economic steps stated as named assumptions rather than silently absorbed, and with the obstructions of compliance composition promoted to first-class price-layer objects — so that the one composition the pricing literature has no vocabulary for, jurisdictional applicability disagreeing across harbors, does not silently become a number.

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.

The price of a claim issued by a multi-harbored entity is conditioned on an admissibility filter. On the fragment where that filter is mechanized law, the conditioning is monotone in the entity’s compliance state and antitone in its harbor set under two named economic assumptions; on the whole composed state space it is faithful to the obstructions of composition. The rest — the full-state-space price map, the adversarial belief distribution, and the net sign of a harbor addition — is named, located in the ledger, and left open.

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.