The Double Fibre of Verification

Maksim Barziankou (MxBv)
Navigational Cybernetics 2.5 · The Urgrund Laboratheory
[e-mail]
DOI: 10.17605/OSF.IO/Z9E5N
Axiomatic Core (NC2.5 v2.1): DOI 10.17605/OSF.IO/NHTC5

Verification can fail twice: a visible artifact may hide the lineage that produced it, while the visible dynamics may hide the admissibility selector under which that lineage should be judged. This finite formal paper models the two losses as a compatible double fibre, proves exact factorisation and reconstruction criteria, and derives the least sufficient visible refinement and its information price.

Hidden Lineage, Hidden Admissibility, and the Contraction of Meaning

Maksim Barziankou (MxBv)

PETRONUS™ · The Urgrund Laboratory · [e-mail]

Poznań · July 2026

License: CC BY-NC-ND 4.0

This work DOI: 10.17605/OSF.IO/Z9E5N

Axiomatic core anchor: NC2.5 v2.1, DOI 10.17605/OSF.IO/NHTC5

Working formal manuscript. Finite, declaration-relative core.

Abstract

Verification can fail even when the visible artifact and its dynamic skeleton are both available: the artifact may hide the lineage that produced it, while the skeleton may hide the admissibility selector under which that lineage should be judged. This paper models the two losses as a compatible double fibre over finite declared histories and selector families. A target verdict factors through the visible representation exactly when it is constant on every double fibre, equivalently when its conditional entropy given the visible representation is zero under a full-support prior. The paper defines a double binding functional, separates hidden-pair ambiguity from target ambiguity, proves a conditional confined-access non-absorption result, and gives explicit crossed, compatibility-cancelled, correlated-prior, and partial-visibility finite models. On the constructive side, every finite target admits a least sufficient visible refinement with a universal property and an exact information price - the residual target entropy - and the gap between hidden-pair binding and target ambiguity is characterised exactly. A separate restriction dynamics yields finite contraction of viable meanings only under stated monotonicity and no-repair premises. Finally, a deterministic pre-commit reference monitor is shown sufficient to enforce decidable prefix-closed safety under authoritative visibility and complete mediation; it is maximally permissive among sound pre-commit monitors, and when the admissibility selector itself is hidden and the declared proposal class carries no selector information, the fibrewise intersection of the candidate safety properties yields the maximally permissive sound commitment rule on the declared proposal surface among monitors confined to the visible channel. The resulting architecture separates verification, reconstruction, property detection, enforcement, revision, liveness, and semantic coordination rather than compressing them into one score.

---

§0. Status and claim ledger

This paper isolates a narrow epistemic structure that recurs across long-horizon verification.

A visible artifact can forget the history that produced it. A visible dynamic skeleton can also forget the admissibility rule under which that history is to be judged. These are different losses. The first is a lineage fibre. The second is an admissibility fibre. Their compatible pull-together is the double fibre of verification.

The paper establishes, in a finite setting, with a full-support prior wherever entropy is scored:

1. an exact factorisation criterion for visible verdicts;
2. a target-fibre witness that refutes exact visible verification;
3. a three-valued maximal sound classifier;
4. a double binding functional and its conditional-entropy decomposition;
5. reconstruction and confined-access non-absorption results;
6. a finite contraction theorem under explicit restriction and no-repair premises;
7. a reference-monitor sufficiency result for decidable prefix-closed safety properties under complete mediation;
8. an exact equality criterion separating hidden-pair binding from target ambiguity;
9. a least-sufficient-refinement theorem: every finite target admits a coarsest visible refinement through which it factors, obtained by adjoining the target's level sets fibrewise, at an exact information price equal to the residual target entropy, with a lattice of sufficient channels above it;
10. maximal permissiveness of the 𝒮-monitor among sound pre-commit monitors, and an intersection-envelope theorem bounding what any monitor confined to the visible channel can soundly enforce on the declared proposal surface when the proposal class carries no selector information - an envelope that is monotone in the compatible selector set, that a genuine selector channel legitimately escapes, and that may widen if the proposal class is itself coupled to the selector;
11. a quantitative floor on approximate visible verdicts - Fano's inequality and the exact fibrewise posterior-mode error - showing that positive target ambiguity bounds every estimator, not only exact ones.

Result 10 carries three declared premises beyond the finite setting: an extension order on histories with downward-closed selectors, each admitting at least one realised history so the intersection keeps the empty run; a realisation map tying event sequences to those histories, the two together making the candidate safety properties derived rather than supplied and their closure conditions consequences rather than assumptions; and a proposal class carrying no selector information, without which the committed prefix is itself a selector channel. Result 7 carries none of these - Theorem 6.2 is stated entirely in terms of one declared property on event sequences, and precedes the enforcement declarations.

The architectural synthesis is new relative to the surrounding corpus in the following limited sense: hidden lineage and hidden admissibility are treated as two typed forgetting operations within one sealed verification problem. The information-theoretic identities, fibre factorisation principle, chain rule, and data-processing inequality are standard; the reference-monitor construction, the safety/liveness boundary, and the maximal-permissiveness pattern are likewise standard, and the References section catalogues the canonical sources.

This paper does not claim that verification is generally impossible, that meaning must always contract, that an isolated verifier is literally non-causal, that positive hidden-state entropy always makes a particular verdict ambiguous, or that a cognitive agent is necessary for enforcement.

The functional severance coordinate from Severance Defect and the Binding Functional remains independent. The present paper extends the reconstructive side of that programme; it does not replace the severance profile.

---

§1. The problem

Suppose two completed processes produce the same visible artifact. They may differ in the order of their internal transitions, in the seams crossed, in the updates missed, or in the witness carried through those transitions. A verifier confined to the artifact cannot distinguish those histories unless the target property is constant across the corresponding observation fibre.

Now suppose the dynamic skeleton itself is visible. Even then, the rule that declares histories admissible may be absent. The same states and transitions can support more than one admissibility selector. A verifier that sees the skeleton but not the selector may therefore lack the rule by which the visible or reconstructed history should be judged.

These failures compose:

(D, h, α) ⟼ (D, O_D(h)).

The map forgets both the hidden history h behind the observation and the admissibility selector α behind the skeleton D.

The central question is:

When does a target verdict factor through the jointly forgotten representation, and what can be stated when it does not?

A second question concerns time. Repeated substitutions, burdens, exclusions, or reinterpretations may contract a set of viable meanings or continuations. That phenomenon is related to hidden lineage and hidden admissibility, but it is not identical to either. It requires a separate update law and separate monotonicity premises.

---

§2. Typed setup

2.1 Dynamic skeletons and histories

Let 𝒟 be a finite declared class of dynamic skeletons. For each D ∈ 𝒟, let:

• ℋ_D be a finite set of typed histories supported by D;
• 𝒴_D be a finite visible codomain;
• O_D:ℋ_D → 𝒴_D be the declared observation map.

A history may encode a transition sequence, a seam sequence, a propagation trace, a retained-memory trajectory, or another typed provenance object. No metaphysical claim is attached to the word history: it is whatever the audit declares and can operationally compare.

An audit may additionally declare a partial order ⊑ on ℋ_D, read as extends: h′⊑h when h continues h′. Every provenance object listed above carries a natural such order, but nothing in §§3-5 uses one, and the models of §5 leave ℋ_D unordered. The order is declared only where it is needed, in §6.6.

2.2 Admissibility selectors

For each D, let 𝔄(D) be a finite declared family of admissibility selectors

α:ℋ_D → {0, 1}.

The family may be restricted by window closure, shift compatibility, burden monotonicity, or another stated axiom system. Those restrictions are part of the declaration. The dynamic skeleton does not determine 𝔄(D) uniquely.

One restriction presupposes the order of §2.1 and is used in §6.6. Call α downward closed when α(h) = 1 and h′⊑h imply α(h′) = 1: a history cannot be admissible while something it extends is not. This is a restriction on the declared family, not a property of selectors in general - the crossed selectors of §5.1 are not downward closed under any strict order on their two histories, which is exactly why §5 leaves ℋ_D unordered.

The structural forgetting map is

U:(D, α) ⟼ D.

Its fibre over D is

ℱ_U(D) = 𝔄(D).

The existence of two selectors in 𝔄(D) is not yet a disagreement about a particular history. It becomes verdict-relevant only when they evaluate some compatible history differently.

2.3 Compatibility

Not every history-selector pair must be admitted as a possible completion. Let

𝒞_D ⊆ ℋ_D × 𝔄(D)

be the declared compatibility relation. A point (h, α) ∈ 𝒞_D means that h and α may jointly occur in the sealed comparison class.

The completed world space is

Θ = ∐_{D ∈ 𝒟}{D} × 𝒞_D.

A world is written θ = (D, h, α).

Compatibility is load-bearing. It may encode typing constraints, construction constraints, empirical exclusions, or coupling rules. It must be fixed before scoring. If it is changed after a target verdict is seen, the audit has changed.

2.4 The two component fibres

For y ∈ O_D(ℋ_D), define the lineage fibre

ℱ_O(D, y) = {h ∈ ℋ_D:O_D(h) = y}.

The admissibility fibre is ℱ_U(D) = 𝔄(D).

These are independent as types of forgetting, not necessarily as random variables. Compatibility can correlate histories and selectors.

2.5 The double fibre

Define the visible map

V:Θ → ∐_{D ∈ 𝒟}{D} × 𝒴_D, V(D, h, α) = (D, O_D(h)).

Definition 2.1 (Double fibre). For an attained visible value v = (D, y),

ℱ_2(D, y) = V^{-1}(D, y) = {(D, h, α):(h, α) ∈ 𝒞_D, O_D(h) = y}.

After suppressing the visible D,

ℱ_2(D, y) ≅ {(h, α) ∈ 𝒞_D:h ∈ ℱ_O(D, y)}.

In general,

ℱ_2(D, y) ⊆ ℱ_O(D, y) × 𝔄(D).

Equality holds only when the declared compatibility relation contains every pair in that product. Calling the double fibre a Cartesian product without checking compatibility is an overclaim.

2.6 Targets

A finite target is a map

Q:Θ → 𝒬.

Important examples are:

1. admissibility verdict
   
   J_{Adm}(D, h, α) = α(h);

2. persistence verdict
   
   J_P(D, h, α) = I_P(h),
   
   where I_P is a declared seam- or witness-preservation criterion;

3. identity-witness label
   
   J_W(D, h, α) = W(h);

4. vector verdict
   
   𝐉 = (J_{Adm}, J_P, J_{Live}),
   
   where J_{Live} is a declared liveness verdict, typed per audit; this paper treats it as an imported coordinate (§13) and proves nothing liveness-specific about it.

The target must be declared before looking at the desired result. Changing from full completion reconstruction to a coarse property after observing a non-identifiability witness changes the question.

---

§3. Exact verification through the visible representation

3.1 Exact visible verification

Definition 3.1. A target Q is exactly verifiable from V on Θ if there exists

q:im(V) → 𝒬

such that

Q = q ∘ V.

The verifier is then confined to the declared visible representation. A constant map for one preselected target world does not count as uniform verification over Θ.

3.2 Factorisation theorem

Theorem 3.2 (Double-fibre factorisation). Let Θ and 𝒬 be finite, and let π be a full-support prior on Θ. The following are equivalent:

1. Q = q ∘ V for some q;
2. Q is constant on every double fibre ℱ_2(D, y);
3. H_π(Q∣V) = 0.

Proof. If Q = q ∘ V, two worlds with the same visible value have the same target, so Q is fibre-constant. If Q is fibre-constant, define q(v) as the common target value on V^{-1}(v); this is well-defined and gives Q = q ∘ V. For finite variables, H(Q∣V) = 0 exactly when Q is almost surely a function of V. Full support converts almost-sure constancy into constancy on every declared fibre. □

The theorem is target-relative. A fibre may contain many hidden completions while a coarse target remains constant.

3.3 Target-fibre witness

Corollary 3.3 (Target-fibre witness). If there exist compatible pairs

(h_0, α_0), (h_1, α_1) ∈ 𝒞_D, θ_0 = (D, h_0, α_0), θ_1 = (D, h_1, α_1),

such that

O_D(h_0) = O_D(h_1) but Q(θ_0) ≠ Q(θ_1),

then no exact V-confined verifier for Q exists on the declared class.

Proof. Compatibility places θ_0 and θ_1 in Θ, and the common visible value places both in the double fibre ℱ_2(D, O_D(h_0)). They carry different target values, so Q is not fibre-constant; Theorem 3.2 then denies factorisation. □

One pair is sufficient. The witness must preserve all visible coordinates and differ in the declared target. A pair that changes an undeclared side channel is not a witness for the original channel. The compatibility requirement is not decorative: a pair drawn from ℱ_O(D, y) × 𝔄(D) but absent from 𝒞_D is not a world at all, and a refutation built on such a pair asserts exactly the product assumption that F6 forbids.

3.4 The maximal sound partial verdict

For binary Q and an attained visible value (D, y) ∈ im(V), define

q^⋆(D, y) = {

1, Q = 1 on all of ℱ_2(D, y),

0, Q = 0 on all of ℱ_2(D, y),

?, otherwise.

}

Proposition 3.4 (Fibre trichotomy). The classifier q^⋆ is sound: whenever it returns 0 or 1, that value equals Q for every compatible hidden completion. It is maximally decisive among all sound V-confined classifiers im(V) → {0, 1, ?}: every heterogeneous target fibre must receive ?. The restriction to V-confined classifiers is what makes the claim non-trivial - a classifier reading θ directly is sound and never returns ?, but it is not a verifier in the sense of Definition 3.1.

Proof. Homogeneous fibres permit their common value. On a heterogeneous fibre, returning either binary value would be wrong for at least one compatible completion. □

The symbol ? means insufficient information under the sealed declaration. It is not a claim that the world itself is indeterminate.

3.5 Vector targets

Proposition 3.5. A finite vector target

𝐐 = (Q_1, …, Q_m)

factors through V if and only if every coordinate Q_i factors through V.

Proof. If 𝐐 = q ∘ V then Q_i = pr_i ∘ q ∘ V for each i. Conversely, if Q_i = q_i ∘ V for every i, then 𝐐 = (q_1, …, q_m) ∘ V. □

Exact recovery of the vector therefore requires fibre constancy of every coordinate separately. This does not forbid some scalar summary from factoring through V: a collapsed score such as Q_1 ∧ Q_2 can be fibre-constant while its constituent coordinates are not. The witness is given in §5.5, where the score factors through V and is non-constant on Θ while neither conjunct factors; a model with a constant observation map can only make the point with a globally constant score, which collapses nothing. What is lost is exactly the coordinate structure: a factoring score carries no uniform information about a non-factoring coordinate, and failure of one coordinate does not logically determine the others.

3.6 Specialisations

Corollary 3.6 (Fibrewise agreement test for the admissibility verdict). J_{Adm} factors through V if and only if for every attained (D, y) and all pairs (h, α), (h′, α′) ∈ ℱ_2(D, y),

α(h) = α′(h′).

Proof. Theorem 3.2 with Q = J_{Adm}; constancy on the double fibre is literally the displayed agreement. □

The test needs no entropy, and it separates the two failure axes: a selector-only witness violates the agreement with h = h′, a lineage-only witness violates it with α = α′.

Remark 3.7 (Support-relative version). For an arbitrary prior π, H_π(Q∣V) = 0 holds if and only if Q is constant on the support restriction ℱ_2(D, y) ∩ supp π of every double fibre of positive mass. Zero-mass completions are invisible to the entropy, so H_π(Q∣V) = 0 is weaker than constancy on the whole of every fibre over Θ: it ignores every world outside supp π. When supp π ≠ Θ, a world outside the support can break whole-fibre constancy while leaving the entropy zero - whether it is a zero-mass world inside a scored fibre or a world in a fibre of zero mass. Exact factorisation on all of Θ is recovered in the full-support case supp π = Θ, the setting of Theorem 3.2. Probabilistic identifiability on a sub-support must not be reported as declaration-wide verification.

3.7 The least sufficient refinement

The negative results above say when the declared channel is too coarse. The constructive counterpart says exactly how much must be added.

Observations are compared by the partitions of Θ they induce. For O_1:Θ → 𝒴_1 and O_2:Θ → 𝒴_2, say that O_2 refines O_1, written O_2 ≽ O_1, when O_2(θ) = O_2(θ′) implies O_1(θ) = O_1(θ′): every O_2-fibre lies inside one O_1-fibre, equivalently O_1 = g ∘ O_2 for some g on the attained values. These observation channels are typed on Θ, unlike the declared observation map O_D of §2.1, which is typed on ℋ_D; the letter is shared, the domains are not. Refinement compares information content, not codomain labels. It is an order on observation channels only - unrelated both to the temporal subdivision of a history into finer steps in the companion seam papers and to the specification-refinement question of §12, problem 8.

Theorem 3.8 (Least sufficient visible refinement). Let Q:Θ → 𝒬 be a finite target. Define

V_Q(θ) = (V(θ), Q(θ)).

Then:

1. V_Q ≽ V, and Q factors through V_Q;
2. V_Q is coarsest with these properties: if O′ ≽ V and Q = f ∘ O′ for some f, then O′ ≽ V_Q;
3. the V_Q-fibres are exactly the intersections of V-fibres with Q-level sets, so the information that must be added to V is exactly the target's level-set partition on each mixed double fibre - and nothing on any homogeneous fibre.

Proof. (1) is immediate from the definition. (2) Suppose O′(θ) = O′(θ′). Then V(θ) = V(θ′) because O′ ≽ V, and Q(θ) = f(O′(θ)) = f(O′(θ′)) = Q(θ′); hence V_Q(θ) = V_Q(θ′), which is O′ ≽ V_Q. (3) restates the definition of V_Q. □

The theorem is the constructive dual of Corollary 3.3. The witness pair says that a mixed fibre defeats every V-confined verifier; the refinement theorem says which further distinctions - and no more - restore the verdict. The refinement V_Q is defined through Q itself, so it specifies the informational content of a sufficient channel, not a procedure the confined verifier could execute: the theorem locates the missing information; it does not conjure it. Which physical instrument realises those distinctions is a separate engineering obligation (§12, problem 2).

Corollary 3.9 (Lattice form).

1. Q = q ∘ V for some q if and only if V ≽ V_Q;
2. for a vector target 𝐐 = (Q_1, …, Q_m), the channel V_𝐐 is the least upper bound of V_{Q_1}, …, V_{Q_m} in the refinement order among observations refining V;
3. if Q_r = r ∘ Q is a coarsening of the target, then V_Q ≽ V_{Q_r}, so exact visibility of Q yields exact visibility of every deterministic summary of Q.

Proof. (1) If V ≽ V_Q, then V_Q = g ∘ V and Q is the second coordinate of g ∘ V; conversely, Q = q ∘ V makes V_Q = (V, q ∘ V) a function of V. (2) V_𝐐 refines every V_{Q_i}; an observation refining V and every V_{Q_i} determines V and every coordinate, hence V_𝐐. (3) Equal V_Q-values force equal (V, r(Q))-values. □

Theorem 3.2 is thus the bottom test of a lattice: the declared channel verifies the target exactly when it already sits above the least sufficient refinement, vector targets join componentwise - which makes Proposition 3.5 constructive - and coarser targets sit lower. The sufficient channels do form a lattice, with V_Q at the bottom. They are closed under join because the common refinement of two channels refining V_Q again refines it, and under meet because the finest common coarsening does too - the join of two equivalence relations contained in the V_Q-relation is contained in it, that relation being transitive. Both closures are immediate; clause (2) is a sharper statement about the specific channels V_{Q_1}, …, V_{Q_m} of a vector target, not the general closure. As with refinement itself, the lattice lives on the induced partitions rather than on the maps.

---

§4. The double binding functional

Let the random world (D, H, A) have full-support law π on Θ, where A is the selector-valued coordinate. Following standard information-theoretic usage, H denotes both the entropy functional and the history-valued coordinate, as in H(H, A∣V); position fixes the reading. Let

Y = O_D(H), V = (D, Y).

4.1 Pointwise and average double binding

Definition 4.1. For an attained v = (D, y),

𝔅_2^π(v) = H_π(H, A∣V = v).

The average double binding is

𝔅̅_2^π = H_π(H, A∣V).

This measures residual uncertainty about the hidden history-selector pair. It does not by itself measure functional damage, computational difficulty, moral quality, or ambiguity of a specific verdict.

Under a uniform posterior on a finite double fibre,

𝔅_2^{unif}(D, y) = log_2|ℱ_2(D, y)|.

4.2 Exact decomposition

Theorem 4.2 (Double binding decomposition).

H(H, A∣V) = H(H∣V)+H(A∣H, V)

= H(H∣V)+H(A∣V)-I(H;A∣V).

Proof. The first line is the conditional chain rule. The second is immediate from the definition I(H;A∣V) = H(A∣V)-H(A∣H, V). □

The terms have distinct meanings:

• H(H∣V) is lineage binding;
• H(A∣V) is visible-selector ambiguity;
• H(A∣H, V) is selector ambiguity remaining after the history is supplied;
• I(H;A∣V) is the dependence correction.

No independence assumption is licensed by the phrase two fibres. The correction can be made positive by either of two distinct mechanisms: a restricted compatibility relation that removes pairs from the support (§5.2), or a correlated prior on a full product support (§5.4). Naming the term after compatibility alone would conflate them; Lemma 4.7 in §4.6 separates the two regimes exactly.

4.3 Verdict ambiguity

Define the target ambiguity

𝔙_Q^π = H_π(Q∣V).

The fraktur 𝔙 is chosen to avoid collision with the visible map V of §2.5.

Proposition 4.3. If Q is a deterministic function of (D, H, A), then

H(Q∣V) ≤ H(H, A∣V).

Proof. Since D is already contained in V, conditional data processing for the deterministic map (D, H, A) ↦ Q yields the inequality. □

Positive double binding is therefore only a capacity for target ambiguity. It does not entail it. The target can be constant on a non-singleton double fibre. Conversely, by the same inequality, positive target ambiguity entails positive double binding: 𝔙_Q^π > 0 forces 𝔅̅_2^π > 0. Proposition 4.8 in §4.6 characterises exactly when the inequality is tight.

4.4 Reconstruction criterion

Proposition 4.4 (Hidden-pair reconstruction). Under a full-support prior on finite Θ, the following are equivalent:

1. every double fibre is a singleton in its hidden pair (H, A);
2. there exists ρ such that ρ(V) = (H, A) on all of Θ;
3. H(H, A∣V) = 0.

Proof. Theorem 3.2 with Q the hidden pair itself. Constancy of that target on a double fibre says the fibre has one hidden pair, which is (1); factorisation through V is the decoder ρ of (2); the entropy clause transfers unchanged. □

This is reconstruction of the declared hidden pair. A coarser lineage label may be reconstructible even when the full history is not. Reconstruction is also the top of the target hierarchy: under full support, H(H, A∣V) = 0 if and only if every finite target factors through V - one direction is Proposition 4.3 applied to an arbitrary target, the other takes the target to be the hidden pair itself.

4.5 Confined non-absorption

Let D be public side information already included in V, and let Z be every datum available to a downstream verifier or upper layer. The symbol Z is used here so that W remains reserved for the identity witness of §8.1.

Definition 4.5. Access is confined to V, conditionally on D, when

(H, A) ⟶ V ⟶ Z∣D

is a conditional Markov chain; equivalently,

I((H, A);Z∣V, D) = 0.

Independent randomness and arbitrary post-processing are allowed; undeclared information about (H, A) is not.

Theorem 4.6 (Confined non-absorption). Under Definition 4.5,

H(H, A∣Z, D) ≥ H(H, A∣V, D) = H(H, A∣V).

Consequently, if H(H, A∣V) > 0, no decoder from (Z, D) can uniformly reconstruct the hidden pair.

If, in addition, H(Q∣V) > 0, then

H(Q∣Z, D) ≥ H(Q∣V, D) = H(Q∣V) > 0,

so no exact verifier based on (Z, D) can recover Q uniformly.

Proof. Conditional data processing gives

I((H, A);Z∣D) ≤ I((H, A);V∣D),

which is equivalent to the hidden-pair entropy inequality. Because D is already a coordinate of V, conditioning on both V and D is the same as conditioning on V. The same conditional Markov relation holds for every deterministic target Q = Q(D, H, A), giving the target-level inequality. □

If D is already retained inside Z, the conditioning on D may be suppressed. The theorem says nothing when a side channel breaks the conditional Markov relation. It also does not prohibit approximation, property detection, emulation, or independent rediscovery.

4.6 Exact regimes

Two exact statements pin down the boundary cases of the decomposition and of Proposition 4.3.

Lemma 4.7 (Product regime). If, conditionally on every attained visible value v, the posterior factorises,

π(h, α∣v) = π(h∣v) π(α∣v),

then I(H;A∣V) = 0 and the double binding is additive: H(H, A∣V) = H(H∣V)+H(A∣V). Conversely, I(H;A∣V) = 0 forces that factorisation on every attained fibre of positive mass, so the two conditions are equivalent; a law that fails to factorise on some such fibre therefore has I(H;A∣V) > 0. A factorised fibre law has product support, so a fibre whose conditional support is not the product of its marginal supports gives I(H;A∣V) > 0 as a special case - one detectable from the support alone, without reference to the numerical law.

Proof. Conditional mutual information vanishes exactly at conditional independence, which is the displayed factorisation; additivity is then Theorem 4.2. The support of a product law is the product of the marginal supports, so a non-product conditional support excludes factorisation on that fibre; that fibre contributes strictly positive conditional mutual information, and every fibre contributes non-negatively. □

The diagonal relation of §5.2 has a non-product conditional support, so its correction is forced; the correlated prior of §5.4 keeps a full product support and produces its correction through the law alone. Removing pairs does not force dependence when the removal leaves a product - deleting every pair containing one history shrinks the support to a smaller product and permits I(H;A∣V) = 0; the non-product condition is the exact trigger.

Proposition 4.8 (Equality criterion). Let π have full support and let Q be a deterministic function of (D, H, A). Then

H(Q∣V) = H(H, A∣V)

if and only if Q is injective on every attained double fibre: for all (h, α), (h′, α′) ∈ ℱ_2(D, y) with (h, α) ≠ (h′, α′), the target values differ.

Proof. Since D is a coordinate of V and Q is a function of (D, H, A), the chain rule gives

H(H, A∣V) = H(Q∣V)+H(H, A∣Q, V).

Equality therefore holds exactly when H(H, A∣Q, V) = 0, that is, when the hidden pair is almost surely determined by the pair (Q, V). Under full support this is determination on every attained fibre, which is the displayed injectivity. □

The gap between double binding and target ambiguity is thus not an accident of the examples: it closes exactly when the target separates every pair of hidden completions that share an observation, and it is strict in every other audit.

Proposition 4.9 (Information budget of repair). Let π have full support.

1. H(V_Q∣V) = H(Q∣V): the least sufficient refinement adds exactly the residual target entropy;
2. every observation O′ ≽ V through which Q factors satisfies H(O′∣V) ≥ H(Q∣V);
3. an added side channel X obeys H(Q∣V, X) = H(Q∣V)-I(Q;X∣V), so repair is monotone; and if X is itself an observation on Θ, the verdict becomes exact precisely when the side channel carries the full residual entropy.

Proof. (1) V_Q = (V, Q), and the chain rule gives H(V, Q∣V) = H(Q∣V). (2) Q is a function of O′, so H(Q∣V) ≤ H(O′∣V). The entropy identity in (3) is the definition of conditional mutual information and needs nothing further; exactness at H(Q∣V, X) = 0 is Theorem 3.2 applied to the enlarged channel (V, X), which is again a map on Θ precisely because X is, and it is there that the full-support hypothesis is used. A randomised or externally seeded side channel still satisfies the identity but is not an observation on Θ, so the exactness reading does not transfer to it. □

Target ambiguity is therefore not only an obstruction measure. It is the exact price, in bits, of the channel that verification lacks: no sufficient enlargement can carry less, and the least one carries exactly that. Falsifier F1's recomputation obligation has a closed form.

---

§5. Minimal finite models

5.1 Fully crossed double fibre

Fix one skeleton D. Let

ℋ_D = {h_0, h_1}, 𝔄(D) = {α_0, α_1},

with

α_0(h_0) = 1, α_0(h_1) = 0,

α_1(h_0) = 0, α_1(h_1) = 1.

Let O_D(h_0) = O_D(h_1) = y, let every pair be compatible, and place the uniform prior on the four worlds.

Then

H(H, A∣V) = 2 bits,

H(H∣V) = 1, H(A∣V) = 1, I(H;A∣V) = 0.

For J_{Adm} = α(H), two worlds are accepted and two rejected, so

H(J_{Adm}∣V) = 1 bit.

The pairs (h_0, α_0) and (h_0, α_1) form a selector-only target-fibre witness. The pairs (h_0, α_0) and (h_1, α_0) form a lineage-only witness. The four-world class exhibits both failures at once.

5.2 Compatibility cancellation

Keep the same histories and selectors, but declare only

𝒞_D = {(h_0, α_0), (h_1, α_1)}.

Under the uniform prior,

H(H∣V) = 1, H(A∣V) = 1, I(H;A∣V) = 1,

and therefore

H(H, A∣V) = 1 bit.

Yet J_{Adm} = 1 on both worlds, so

H(J_{Adm}∣V) = 0.

This model proves two points at once: the double fibre need not be a product, and positive double binding need not make the admissibility verdict ambiguous.

5.3 Four diagnostic regimes

For a fixed visible value, the following regimes are distinct:

Lineage multiplicity	Selector multiplicity	Hidden-pair status
1	1	pair reconstructible
> 1	1	lineage ambiguity only
1	> 1	selector ambiguity only
> 1	> 1	both axes present, subject to compatibility

This table classifies hidden completions, not verdicts. The first row is a singleton fibre, so every target is constant on it by construction; each of the remaining rows can still contain either a homogeneous or a heterogeneous target fibre. The minimal models of §5.1, §5.2, §5.4 and §5.5 all realise the last row; the intermediate rows are reached by restricting compatibility so that only one axis retains multiplicity. Restricting §5.1 that way fixes the verdict pattern as well, so the homogeneous sub-cases of rows 2 and 3 need either a coarser target or selectors declared in no model here.

5.4 Dependence without restriction

Keep the fully crossed compatibility relation of §5.1 - every pair (h_i, α_j) admitted - but replace the uniform prior by the correlated full-support law

π(h_0, α_0) = π(h_1, α_1) = 1/2-ε, π(h_0, α_1) = π(h_1, α_0) = ε,

for ε ∈ (0, 1/2) with ε ≠ 1/4. Both hidden marginals remain uniform, so with h_2 the binary entropy function,

H(H∣V) = H(A∣V) = 1, H(H, A∣V) = 1+h_2(2ε), I(H;A∣V) = 1-h_2(2ε) > 0,

and the admissibility verdict has H(J_{Adm}∣V) = h_2(2ε). At ε = 1/8 the dependence correction is exactly 3/4 log_2 3-1 bits.

No pair has been excluded: the support is the full product, yet the dependence correction is positive because the fibre law does not factorise (Lemma 4.7). Support restriction (§5.2) and prior correlation are therefore independent mechanisms for coupling the two fibres, and an audit that observes I(H;A∣V) > 0 cannot conclude that the compatibility relation was restricted.

5.5 Partial visibility

The three models above share a constant observation map, so the visible codomain of each is a single point. That suffices to exhibit binding, cancellation and dependence, but it degenerates three things at once: factorisation through V collapses to global constancy, the least sufficient refinement of Theorem 3.8 is instantiated only where V carries no information, and the detectability regime of §8.3 has no instance, since a constant V forces I(P;S^⋆∣D) = 0 for every property. The following model separates the visible values.

Fix one skeleton D. Histories are written g_i here rather than h_i, so that no index collides with the binary entropy h_2 of §5.4. Let

ℋ_D = {g_0, g_1, g_2, g_3}, 𝔄(D) = {α_0, α_1},

with

α_0 admitting {g_0, g_2}, α_1 admitting {g_1, g_3},

let every pair be compatible, and let

O_D(g_0) = O_D(g_1) = y_0, O_D(g_2) = O_D(g_3) = y_1.

Place the uniform prior on the eight worlds. The selector values are declared for typing - a selector must be total on ℋ_D - and the quantities below do not depend on them, since the target P is a function of the history alone. Let P be the property taking value 1 on g_0, g_1, g_2 and 0 on g_3, and take the declared statistic S^⋆ = V.

Each double fibre carries four hidden pairs, so

H(H, A∣V) = 2 bits.

The y_0 fibre is P-homogeneous and the y_1 fibre is mixed, so

H(P∣V) = 1/2, H(P) = h_2(1/4) = 2-3/4 log_2 3, I(P;S^⋆∣D) = 3/2-3/4 log_2 3 > 0.

Three conditions hold simultaneously: the hidden pair is not reconstructible, the property is not exactly verifiable from V, and the property is statistically detectable. This is the regime described in §8.3, and it is the first model here to instantiate it. The leakage is saturated rather than small - I((H, A);V∣D) = H(Y∣D) = 1 bit, the whole capacity of a binary visible channel - so the model witnesses the regime, not the narrow-channel reading of it.

The same model supplies a non-degenerate witness for Proposition 3.5. Let

Q_1 = P, Q_2 = 1 on {g_0, g_1, g_3}, 0 on {g_2}.

On the y_1 fibre Q_1 reads (1, 0) and Q_2 reads (0, 1), so neither coordinate factors through V. Their conjunction is 1 on {g_0, g_1} and 0 on {g_2, g_3}, constant on each fibre and non-constant on Θ, so the collapsed score factors while no constituent does. This is the genuine collapse: a score that carries no uniform information about either coordinate it was built from. The crossed model of §5.1 can make the point only with a globally constant score, which collapses nothing.

---

§6. Verification, enforcement, and revision

6.1 Five roles

A verification architecture should distinguish at least five roles:

1. producer - emits the artifact or proposes a transition;
2. observation channel - exposes the declared V;
3. verifier - computes a target or partial verdict;
4. enforcer - can block or commit the proposed transition;
5. revision authority - may change the selector, observation contract, or system version.

These roles may be implemented by one machine, but their authorities remain different. Detection of a violation does not entail authority to block it. Authority to block does not entail authority to revise the rule. Visibility of the boundary does not entail optimizer query, gradient, or write access to that boundary.

6.2 Structural and transaction-level admissibility

Let 𝒜_h be an action set, ℰ_h an effect space, and

e_h:𝒜_h → ℰ_h

the declared effect map. Let

Adm_h^{str}:ℰ_h → {0, 1}

be a structural predicate over effects.

The exact executable pullback is

G_h^{str}(a) = Adm_h^{str}(e_h(a)).

A policy or credential gate G_h^{txn} is a different object. It may equal the pullback, be stricter, or admit actions whose long-horizon effect is structurally destructive.

Let R_h ⊆ 𝒜_h be the declared reachable action set: the actions that can actually be executed in the audited run class. (Throughout this subsection the subscript h names the audited context and is fixed.) A run has clean transaction-level records when every executed action a satisfies G_h^{txn}(a) = 1. Call the run class rich when every gate-passing action in R_h is executed by at least one run with clean records - any class closed under single-action runs is rich.

Proposition 6.1 (Transaction-to-structure correspondence). For a rich run class, clean transaction-level records entail structural admissibility of every executed effect if and only if

G_h^{txn}(a) ≤ Adm_h^{str}(e_h(a)) for every a ∈ R_h.

Equality on R_h additionally makes the executed gate an exact implementation of the structural pullback on the reachable support.

Proof. If the domination holds, every executed action of a clean-record run passes the gate and therefore has a structurally admissible effect; richness is not needed for this direction. If the domination fails at some a^⋆ ∈ R_h, then G_h^{txn}(a^⋆) = 1 while Adm_h^{str}(e_h(a^⋆)) = 0; richness supplies a clean-record run executing a^⋆, and that run has a structurally inadmissible effect. □

Without richness the converse can fail vacuously: if every run reaching a gate-passing bad action also executes a gate-failing one, no clean run witnesses the defect, and the entailment holds while the domination does not.

One-sided domination on the reachable support is the whole correspondence obligation; agreement with the pullback outside R_h is not required. The problem is not that a Boolean gate is inherently too shallow. A Boolean gate can implement a rich geometry exactly. The defect is a missing or false domination through the effect map and structural kernel.

6.3 Reference-monitor sufficiency

Let E be a finite typed event alphabet and let

𝒮 ⊆ E^⋆

be a decidable prefix-closed safety property with ϵ ∈ 𝒮.

A pre-commit monitor holds the current committed prefix p and, on a proposed event e, either commits it or rejects that event and continues; a rejected event leaves p unchanged and the run is not terminated. This is the disable-a-controllable-event semantics of supervisory control, not truncation: rejecting a proposed step suppresses that step, it does not halt the process. This names a class: the decision rule is not yet fixed. The 𝒮-monitor is the member that commits e exactly when pe ∈ 𝒮.

Theorem 6.2 (Safety enforcement under complete mediation). If:

1. every committed event is visible to the monitor;
2. every event is committed only through the monitor - no unmediated commit path exists;
3. the monitor evaluates the authoritative prefix;
4. the decision procedure for membership in 𝒮 is correct;
5. ϵ ∈ 𝒮, equivalently 𝒮 is non-empty;

then, at every step, the authoritative committed prefix of the mediated system coincides with the prefix held by the 𝒮-monitor and remains in 𝒮.

Proof. Hypotheses 1--3 couple the system trace to the monitor state: every system commit is visible to the monitor, no commit can bypass it, and the prefix evaluated by the monitor is the authoritative committed prefix. The base case is hypothesis 5, with both prefixes equal to ϵ. Assume the common current prefix is p ∈ 𝒮. If the 𝒮-monitor accepts a proposed event e, correctness of the decision procedure gives pe ∈ 𝒮 and complete mediation advances both prefixes to pe. If it rejects e, complete mediation prevents a system commit and both prefixes remain p. Induction proves both coincidence and safety. □

A cognitive agent and model-family heterogeneity are unnecessary for this enforcement result. They may be useful for proposing invariants, interpreting evidence, or auditing a monitor, but they are not premises of the theorem.

The theorem does not guarantee liveness, availability, semantic convergence beyond the predicate, recovery after monitor failure, or safety under incomplete mediation. Prefix-closedness is what makes 𝒮 a safety property in the classical sense of Alpern and Schneider. The induction uses correctness of the decision procedure, ϵ ∈ 𝒮, and the exact system-to-monitor coupling supplied by authoritative visibility and complete mediation. Decidability is an implementability condition on the monitor, not a premise of the induction.

Proposition 6.3 (Maximal permissiveness). Call a pre-commit monitor sound when every prefix it commits lies in 𝒮. Among sound pre-commit monitors, the 𝒮-monitor is stepwise maximally permissive: at every reachable committed prefix p ∈ 𝒮 it commits a proposed event e exactly when some sound monitor at p could commit it, namely when pe ∈ 𝒮.

Proof. Soundness forbids committing e at p when pe ∉ 𝒮. The 𝒮-monitor commits in every remaining case. □

Safety alone is achievable by the monitor that rejects everything; maximal permissiveness is what makes the construction non-trivial. Because the monitor can veto every event, this is the degenerate all-events-controllable case of the supremal-sublanguage pattern of supervisory control. Whether a committed prefix retains admissible continuations is a liveness question and remains outside the theorem.

6.4 Isolation and return channels

Isolation is a channel restriction:

hidden world ⟶ V ⟶ verifier.

It is not literal non-causality. A verifier may return a minimal verdict to an enforcer without exposing the raw provenance or a gradient-bearing boundary to the optimizer.

If detailed findings are used to revise the producer, the result is a new artifact, a new history, and a new audit epoch. Feedback is not forbidden; it changes the object being verified. The safe statement is therefore:

raw audit information must not silently alter the object inside the same certification claim.

6.5 Failure and unknown policies

The fibre trichotomy introduces ?. An implementation must declare what ? does:

• fail closed;
• fail open;
• halt propagation;
• escalate to a privileged audit;
• request a new observation;
• defer until a bounded recovery procedure completes.

The mathematical fibre result does not choose among these policies. Each choice has distinct safety, liveness, and denial-of-service consequences.

6.6 Enforcement under hidden admissibility

The 𝒮-monitor of §6.3 presumes one declared safety property. Under the double fibre, the intended property may itself depend on the hidden selector, while the true α stays hidden from the monitor. Making that dependence structural rather than nominal requires one declaration, because selectors are typed on histories (§2.2) and safety properties on event sequences (§6.3); nothing said so far connects E^⋆ to ℋ_D.

Declaration (runs and histories). Let

ι:E^⋆ ⟶ ℋ_D

be the declared realisation map, sending a run to the history it realises. This subsection declares three things beyond §§2-5: the extension order ⊑ on ℋ_D of §2.1; that every α ∈ 𝔄(D) is downward closed in the sense of §2.2; and that ι is total, computable, and order-preserving,

q ≼ p ⟹ ι(q)⊑ι(p),

where ≼ is the prefix order on E^⋆. Since ϵ ≼ p for every run, ι(ϵ) is ⊑-below every realised history.

Each selector then induces a safety property by pullback,

𝒮_α = {p ∈ E^⋆:α(ι(p)) = 1},

so that {𝒮_α}_{α ∈ 𝔄(D)} is determined by 𝔄(D) rather than merely indexed by it. The two conditions Theorem 6.2 needs are now consequences, not further declarations.

Prefix closure. Let q ≼ p with p ∈ 𝒮_α. Order-preservation gives ι(q)⊑ι(p), and downward closure of α turns α(ι(p)) = 1 into α(ι(q)) = 1; hence q ∈ 𝒮_α.

Initial admissibility. If α admits any realised history at all, then ι(ϵ) lies below it and downward closure gives α(ι(ϵ)) = 1, so ϵ ∈ 𝒮_α.

Decidability. Immediate from computability of ι and finiteness of ℋ_D.

These are sufficient conditions, not characterisations: a pullback family can be prefix-closed while some selector fails downward closure, so the converse does not hold and is not claimed. What the declaration buys is that the closure conditions of §6.3 need not be assumed separately for each 𝒮_α - they follow from the order, the selectors, and ι together.

For an attained visible value v = (D, y), let

𝔄_v = {α:∃h, (h, α) ∈ 𝒞_D, O_D(h) = y}

be the selectors compatible with v. Call a monitor V-confined when its commit decisions depend only on v, the committed prefix, and the proposed event - never on α.

Soundness must be stated per world, and it needs one further declaration. Let Σ be the declared class of event streams the producer may emit. Call the proposal class selector-free when every stream in Σ may be emitted in every world of the fibre over v, so that the producer's choice carries no information about α. Whether Σ has this property is part of the declaration, not a consequence of confinement.

Call a monitor sound in every compatible world when, for each α ∈ 𝔄_v, each stream in Σ, and each prefix the monitor commits while running in a world with selector α, that prefix lies in 𝒮_α. This constrains a monitor only by the property in force in the world it is actually running in; it does not presume the monitor satisfies every member of the family at once.

Theorem 6.4 (Intersection envelope). Assume every selector in 𝔄_v admits at least one realised history - equivalently α(ι(ϵ)) = 1 for each α ∈ 𝔄_v, by initial admissibility. Let

𝒮_∩ = ⋂_{α ∈ 𝔄_v}𝒮_α.

Then:

1. 𝒮_∩ is decidable, prefix-closed, and contains ϵ;
2. the 𝒮_∩-monitor is V-confined and sound in every compatible world;
3. under a selector-free proposal class, every V-confined monitor that is sound in every compatible world commits only prefixes in 𝒮_∩, and the 𝒮_∩-monitor is stepwise maximally permissive at every decision point reached by a monitor in that comparison class on a stream in Σ.

Proof. (1) Each 𝒮_α contains ϵ by the admission hypothesis, and a finite intersection of decidable prefix-closed sets each containing ϵ is decidable, prefix-closed, and contains ϵ. (2) The monitor consults only v, the prefix, and the proposed event; every committed prefix lies in 𝒮_∩ ⊆ 𝒮_α for each compatible α, hence in the property in force in whichever world it runs. (3) Let a V-confined monitor commit p while running in a world with selector α_0 ∈ 𝔄_v, on a stream σ ∈ Σ. Its decisions read only v, the committed prefix, and the proposed event, so the same run on σ commits p in every world of the fibre over v; a selector-free proposal class makes σ available in each of them, so p is committed under every α ∈ 𝔄_v. Soundness in each of those worlds gives p ∈ 𝒮_α for every compatible α, that is p ∈ 𝒮_∩. Now consider any decision point (p, e) reached by a monitor in this comparison class on a stream in Σ. If such a monitor commits e, the preceding argument applied to the resulting prefix pe gives pe ∈ 𝒮_∩; if pe ∉ 𝒮_∩, no monitor in the class can commit it soundly, while the 𝒮_∩-monitor commits whenever pe ∈ 𝒮_∩. This is the claimed Σ-relative stepwise maximality. □

Confinement is what carries clause 3: it transports a prefix committed in one world to every other world of the fibre, and the per-world soundness requirements then intersect. Both premises are load-bearing and fail in different ways. Without confinement, claim 3 fails as shown in Remark 6.5. Without a selector-free proposal class it fails for a second and distinct reason: if some streams are unavailable under some compatible selectors, a committed prefix need not be reachable under all of them, and the monitor is bound only by the smaller family

𝔄_{(v, p)} = {α ∈ 𝔄_v: p is reachable under α},

whose intersection ⋂_{α ∈ 𝔄_{(v, p)}}𝒮_α may be strictly larger than 𝒮_∩. A proposal class coupled to the selector is therefore itself a channel: the committed prefix carries selector information that v does not, and F1 applies at the enforcement layer.

A worked instance. Let E = {s, a, b}, where s is uncontested and a, b are each contested by one selector. Let

ℋ_D = {h_⊥, h_a, h_b, h_⊤}, h_⊥⊑h_a⊑h_⊤, h_⊥⊑h_b⊑h_⊤,

so a history records which contested events have occurred. Let ι(p) be h_⊥ when p contains neither a nor b, h_a when it contains a but not b, h_b when it contains b but not a, and h_⊤ when it contains both. A prefix cannot contain a letter its extension lacks, so ι is order-preserving. Let α_0 admit {h_⊥, h_a} and α_1 admit {h_⊥, h_b} - both downward closed - with a constant observation and every pair compatible, so 𝔄_v = {α_0, α_1}.

The pullback then yields, without further declaration,

𝒮_{α_0} = {p:p has no b}, 𝒮_{α_1} = {p:p has no a}, 𝒮_∩ = {s}^⋆,

each prefix-closed and each containing ϵ by the derivation above. The intersection is not the trivial {ϵ}: on the stream s s a b s the 𝒮_∩-monitor commits sss, rejecting only the contested events, while the monitor that rejects everything commits ϵ. Both are sound; only the first is permissive, which is the content of Proposition 6.3 made visible.

Remark 6.5 (Confinement is load-bearing, and the price is monotone). Claim 3 fails for selector-aware monitors. In the worked instance, a monitor with a channel to the true selector may commit a exactly under α_0 and b exactly under α_1 - sound in every world, since a ∈ 𝒮_{α_0} and b ∈ 𝒮_{α_1}, while committing outside 𝒮_∩ in each. The envelope is the price of hiddenness, not of soundness. That price is monotone: if 𝔄_v ⊆ 𝔄_v^′, then ⋂_{α ∈ 𝔄_v^′}𝒮_α ⊆ ⋂_{α ∈ 𝔄_v}𝒮_α - each additional compatible selector weakly shrinks what a confined monitor may commit, and any refinement of the visible channel that shrinks 𝔄_v weakly enlarges it. The fibre trichotomy dualises at the enforcement layer: a prefix in 𝒮_∩ is admissible under every compatible selector, a prefix outside ⋃_{α ∈ 𝔄_v}𝒮_α under none, and the region between is the enforcement-side ?.

Enforcement under hidden admissibility therefore pays an exact price: with a selector-free proposal class and no channel to α, no committed prefix reached on a stream in Σ can lie outside the compatible intersection for a sound confined monitor, and the intersection rule is stepwise maximally permissive on that declared proposal surface. A monitor that, while the selector is hidden, commits prefixes outside 𝒮_∩ under the banner of enforcing some particular 𝒮_{α_0} ⊋ 𝒮_∩ is in at least one of three positions: it is unsound for another compatible selector; or it is silently using an undeclared selector channel; or the declared proposal class is coupled to the selector, so that the committed prefix is itself such a channel and the operative envelope is the one over 𝔄_{(v, p)}. The three are not exclusive - a monitor may read the selector and be unsound as well.

What the envelope is not. It is tempting to read 𝒮_∩ as the enforcement-side image of target ambiguity, so that the verifier's mixed fibre becomes the enforcer's intersection. That reading is wrong in both directions, and this paper's own models refute it. The envelope is a function of the compatible selector family 𝔄_v - its members and their induced safety properties, not its cardinality alone - whereas target ambiguity H(Q∣V) measures how a declared target varies across the whole double fibre.

A mixed fibre need not contract the envelope. Reuse the worked instance's downward-closed α_0, admitting {h_⊥, h_a}, as the only compatible selector, over runs that realise h_b and h_⊤ as well. The admissibility verdict α_0(ι(⋅)) is then mixed across the realised histories - a lineage-only witness in the sense of §3.6. But 𝔄_v = {α_0}, so 𝒮_∩ = 𝒮_{α_0} and nothing is given up at all.

A homogeneous fibre may contract it. Keep both downward-closed selectors α_0, α_1 of the worked instance, but restrict compatibility to the worlds each one admits - (h_⊥, α_0), (h_a, α_0), (h_⊥, α_1), (h_b, α_1). Every compatible world is then admissible, so H(J_{Adm}∣V) = 0 and the verifier's fibre is homogeneous. Yet both selectors occur, so 𝔄_v = {α_0, α_1} and 𝒮_∩ = {s}^⋆ is strictly smaller than either 𝒮_{α_0} or 𝒮_{α_1}, which differ on the realised histories h_a and h_b.

Identifying the two would be precisely the conflation F5 names. What survives is exact and weaker: hidden lineage prices verification, hidden admissibility prices enforcement, and the two prices are charged on different quantities. The role of ι is to make the enforcement price computable from the declared selectors at all - without it, {𝒮_α} is a family the audit must supply by hand, and the closure conditions of §6.3 must be assumed rather than derived.

---

§7. Contraction of meaning

7.1 A separate dynamic object

Let Ω_M be a finite declared universe of meanings, interpretations, continuations, or generators. Let

M_t ⊆ Ω_M

be the set remaining viable at time t.

The word meaning is operational here: membership in M_t must be determined by a declared compatibility or viability criterion. The theorem below does not identify semantic meaning with Shannon entropy.

7.2 Restriction dynamics

Assume a sequence of declared restrictions R_t ⊆ Ω_M and the update

M_{t+1} = M_t ∩ R_t.

Theorem 7.1 (Finite monotone contraction). Under this update:

1. M_{t+1} ⊆ M_t for every t;
2. the set can change strictly at most |M_0| times;
3. if non-emptiness is required, it can change strictly at most |M_0|-1 times;
4. the sequence eventually stabilises.

Proof. Intersection gives nesting. Every strict inclusion of finite sets removes at least one element. There are only |M_0| elements to remove, or |M_0|-1 if one must remain. Therefore only finitely many strict changes can occur, after which the nested sequence is constant. □

For M_{t+1} ≠ ∅, define the contraction increment

κ_t = log_2(|M_t|/|M_{t+1}|) ≥ 0.

For s < t with every intermediate set non-empty,

∑_{k = s}^{t-1}κ_k = log_2(|M_s|/|M_t|).

If M_{t+1} = ∅, the logarithmic score is not finite; collapse must be reported separately.

7.3 What the theorem does not say

Contraction is not inevitable. If R_t ⊇ M_t, then M_{t+1} = M_t. A repair, capacity increase, reinterpretation, or expansion operator can also violate the intersection update.

Therefore a claim of unavoidable contraction needs, at minimum:

1. a fixed comparison type Ω_M;
2. a declared update law;
3. monotone restriction or burden-to-viability correspondence;
4. no unmodelled repair or capacity growth;
5. at least one strict restriction if strict contraction is claimed.

A non-zero burden variable alone does not prove that |M_t| decreases.

7.4 Epistemic and ontic contraction

A consistent-generator set

Cons_{t+1} = Cons_t ∩ {γ:γ fits evidence e_{t+1}}

may contract because knowledge improves. This is epistemic contraction.

A viable-continuation set M_t may contract because possible futures are actually removed. This is ontic or operational contraction.

The first does not entail the second. Learning which generator produced a trace can reduce uncertainty while enlarging the set of actions the observer knows to be safe. Those are different objects: the intersection update of §7.2 governs M_t and can only shrink it, whereas knowing an action to be safe is a fact about the observer's information rather than membership in the declared universe Ω_M. Reporting epistemic gain as ontic expansion is exactly the conflation this subsection separates. Conversely, viable futures can disappear while the observer remains uncertain about why.

7.5 Relation to the double fibre

For each hidden completion (D, h, α), a declared rule may assign a continuation set

M_t = M_t(D, h, α).

Corollary 7.2 (Visible identifiability of contraction). Fix the declared assignment and a contraction statistic Q_t - for instance Q_t = |M_t|, or Q_t = κ_t on steps with M_{t+1} ≠ ∅. Then Q_t is exactly verifiable from V if and only if Q_t is constant on every double fibre.

Proof. Theorem 3.2 applied to the target Q_t. □

The condition genuinely fails in small models: in the crossed model of §5.1, declare M_0 = {m_1, m_2} for every world and the rule M_1(D, h, α) = M_0 if α(h) = 1 and M_1(D, h, α) = {m_1} otherwise. Then κ_0 = 0 on the accepted worlds and κ_0 = 1 on the rejected ones, while all four worlds share one visible value: two hidden completions carry the same artifact and different remaining meanings.

Contraction therefore lives inside the hidden completion and can be queried through the factorisation theorem. It is not a third fibre unless a third, independently typed forgetting map is introduced.

---

§8. Witness, liveness, and weaker property detection

8.1 Retained memory and witness factorisation

Let

Ret:ℋ_D → ℛ_D

be a retention map from full history to retained state, and let

W:ℋ_D → 𝒲

be an identity-relevant witness.

Proposition 8.1. There exists W̃ with

W = W̃ ∘ Ret

if and only if W is constant on every retention fibre.

Proof. The factorisation argument of Theorem 3.2 with Ret in place of V: if W = W̃ ∘ Ret, two histories with equal retained state carry equal witnesses; conversely, fibre constancy makes W̃(r) the common value on Ret^{-1}(r) well defined. □

Stored records are therefore not automatically identity-preserving. A copy, fork, or replay may retain the same record without selecting one numerical continuation. The witness and the equivalence relation must be declared.

8.2 Persistence and admissibility

A transported witness can remain intact while the resulting history is inadmissible under the current selector. Conversely, an admissible transition can lose a chosen witness. These are different target coordinates.

A vector such as

(J_{Adm}, J_W, J_{Live})

must be audited coordinate by coordinate. Exact recovery of any declared vector requires fibre constancy of every coordinate.

8.3 Property detection without reconstruction

Let P = P(D, H, A) be a finite property and let S^⋆ = s(V) be a declared statistic of the visible channel. Work at fixed D, or condition throughout on D.

Assume:

I(P;S^⋆∣D) > 0

as an explicit detectability premise, and suppose the hidden-pair leakage obeys

I((H, A);V∣D) ≤ ε.

Then data processing gives

0 < I(P;S^⋆∣D) ≤ I((H, A);V∣D) ≤ ε.

This is compatible with positive residual entropy

H(H, A∣V, D) > 0.

Detectability is therefore compatible with non-reconstructibility, and the displayed chain bounds it from above rather than establishing it: I(P;S^⋆∣D) > 0 is an assumed premise, not a conclusion, and what the chain adds is that no more property information can be present than the visible channel leaks about the hidden pair. The model of §5.5 instantiates the regime - there H(H, A∣V) = 2 while I(P;S^⋆∣D) = 3/2-3/4 log_2 3 > 0 - and no model with a constant observation map can, since a constant V forces I(P;S^⋆∣D) = 0. Positive property information does not yield an exact target verdict, a pointwise witness for every fibre, or identification of the full architecture.

The leakage bound is less general than it looks. Since V is a deterministic function of (D, H), the quantity I((H, A);V∣D) equals H(Y∣D): the ceiling on detectability is the visible channel's own entropy, so a narrow channel bounds every property statistic at once. The detectability premise is in addition conditional on the declared property, statistic, ensemble, and calibration discipline. It is not derived from non-reconstructibility alone.

Remark 8.2 (Quantitative bridge). Positive target ambiguity is not only an obstruction to exact verification but a floor on approximate visible verdicts. For a finite target Q with |𝒬| = n_Q and any estimator Q̂ = g(V), Fano's inequality gives

h_2(Pr[Q̂ ≠ Q])+Pr[Q̂ ≠ Q]log_2(n_Q-1) ≥ H(Q∣V),

so for binary Q the error obeys h_2(Pr[Q̂ ≠ Q]) ≥ H(Q∣V). Fano holds for every estimator without further structure, though its value H(Q∣V) is itself prior-dependent; for any declared prior the exact optimum is

Pr[Q̂ ≠ Q]_{min} = 1-∑_vπ(v) max_{u ∈ 𝒬}π(u∣v),

attained by the fibrewise posterior mode. In the crossed model of §5.1 both readings give exactly 1/2 - no better than ignoring the artifact altogether.

---

§9. Coordination as an implementation condition

Let S_k be an authoritative committed state at version k. Agent i has applied frontier v_i ≤ k, typed projection P_i(S_{v_i}), and operational context C_i.

Define version lag

L_i = k-v_i.

A finite lag bound limits one kind of lineage divergence: the number of authoritative commits omitted from the agent's local history. It does not by itself bound semantic or behavioural divergence. That requires:

1. a projection-conformance condition;
2. a declared observable metric;
3. a stability modulus linking context error to verdict or action error;
4. a recovery protocol for cold start and partial propagation.

Two agents may hold byte-identical logs and still apply different interpreters or selector versions. Conversely, agents may hold different typed projections yet remain behaviourally equivalent on a sealed probe class.

Within the present framework:

• missed or reordered updates are hidden lineage;
• different local predicate versions are hidden admissibility;
• the coordination protocol controls how large those fibres can become in operation;
• a reference monitor that takes no part in the agents' semantic protocol can enforce a declared safety invariant without claiming semantic identity among them; it is not thereby a passive observer, since Theorem 6.2 requires it to mediate the commit path in full.

Propagation halt is an authority, not a proof. It is useful only if the halt surface is completely mediated, scoped, recoverable, and paired with an explicit fail policy.

---

§10. Sealed finite reference audit

The minimal reference audit is fully enumerable.

10.1 Declaration

The audit runs the models of §5 and the enforcement layer of §§6-7. The core information-theoretic declaration is:

• one skeleton D;
• histories {h_0, h_1};
• selectors {α_0, α_1};
• a constant observation O_D(h_0) = O_D(h_1) = y;
• one of the two compatibility relations of §5.1 or §5.2;
• a full-support prior, uniform or the correlated prior of §5.4;
• targets J_{Adm}, H, A, and any chosen persistence target.

Two further declarations, needed by outputs that the constant-observation core cannot express, are run alongside it:

• the partial-visibility declaration of §5.5 - four histories {g_0, …, g_3}, the two-valued observation O_D, the property P, the selectors α_0, α_1 admitting {g_0, g_2} and {g_1, g_3}, and S^⋆ = V - which is the only model instantiating the detectability regime of §8.3 and the only non-degenerate witness for Proposition 3.5;
• the enforcement declaration of §6.6 - the event alphabet E = {s, a, b}, the ordered histories h_⊥⊑h_a, h_b⊑h_⊤, the realisation map ι, downward-closed selectors, and the induced family {𝒮_α} - together with the contraction universe Ω_M and restriction sequence {R_t} of §7.2.

These are distinct sealed declarations; a companion must keep them apart and never carry a label from one into another.

10.2 Required outputs

A companion verifier should:

1. enumerate Θ;
2. group worlds by V;
3. list each double fibre;
4. test target constancy on every fibre;
5. emit an explicit target-fibre witness when constancy fails;
6. compute H(H, A∣V);
7. compute H(H∣V), H(A∣V), and I(H;A∣V);
8. verify the chain-rule identity exactly up to a declared numerical tolerance;
9. compute H(Q∣V);
10. verify the maximal three-valued classifier;
11. rerun after replacing the crossed compatibility relation by the diagonal relation;
12. verify the fibrewise agreement test of Corollary 3.6 on both compatibility relations;
13. construct the least sufficient refinement of Theorem 3.8 on the partial-visibility model and verify both halves of its universal property by enumerating every partition of the eight-world class, confirming the quantifier is non-vacuous;
14. verify the equality criterion of Proposition 4.8 in both directions;
15. verify the product regime of Lemma 4.7 and the correlated-prior model of §5.4, including the closed form I(H;A∣V) = 1-h_2(2ε);
16. run the 𝒮-monitor of Theorem 6.2, the maximal-permissiveness comparison of Proposition 6.3, the transaction-to-structure domination of Proposition 6.1 with a positive and a negative instance, the contraction ledger of Theorem 7.1 with the Corollary 7.2 witness, and the Fano floor of Remark 8.2;
17. verify the lattice form of Corollary 3.9, the reconstruction-top equivalence of §4.4, the information budget of Proposition 4.9, the confined non-absorption inequality of Theorem 4.6, the exact fibrewise posterior-mode floor of Remark 8.2, and the target-level data-processing bound of Proposition 4.3;
18. on the partial-visibility declaration of §5.5: confirm H(H, A∣V) = 2, H(P∣V) = 1/2, and I(P;S^⋆∣D) = 3/2-3/4 log_2 3; check that P does not factor through V; verify the Proposition 3.5 witness in which the conjunction factors while neither conjunct does; and confirm the §5.5 selector declaration admits one history per visible fibre;
19. on the enforcement declaration of §6.6: derive {𝒮_α} from ι and the downward-closed selectors, confirm each is prefix-closed and contains ϵ, run the 𝒮_∩-monitor to a non-trivial committed prefix, exhibit the selector-aware escape of Remark 6.5, and verify the monotone envelope; then confirm both coupled witnesses that the envelope tracks the compatible selector family and not target ambiguity - a single-selector model whose mixed verdict leaves 𝒮_∩ = 𝒮_{α_0} uncontracted, and a two-selector model whose homogeneous verdict still contracts 𝒮_∩ strictly below each member.

10.3 Expected checks

For the crossed model:

𝔅̅_2 = 2, H(J_{Adm}∣V) = 1.

For the diagonal model:

𝔅̅_2 = 1, H(J_{Adm}∣V) = 0,

and the dependence correction is one bit.

For the correlated-prior model of §5.4 at ε = 1/8:

𝔅̅_2 = 1+h_2(1/4) = 3-3/4 log_2 3, I(H;A∣V) = 3/4 log_2 3-1, H(J_{Adm}∣V) = 2-3/4 log_2 3.

The code should use only the sealed declaration. It must not infer hidden labels from filenames, enumeration order, or metadata outside V.

10.4 Extension tests

The executable companion of §10.5 provides finite executable witnesses and checks for items 1-19: the four information-theoretic models, a coarse target that factors through the two-valued observation of §5.5, the finite contraction sequence with telescoping κ_t, and the enforcement layer. A later harness can still add:

• a side-channel variable and demonstrate the change from V to V′ = (V, X);
• a propagation trace with bounded version lag but divergent local selector copies.

These are separate tests. Passing one must not be reported as passing the others. The list above is a coverage map, not a claim that every clause has an independent failure marker. Some identities are structural consequences of the declared constructors, and some named checks are deliberately shadowed by an upstream biting invariant; the audit labels those cases explicitly.

10.5 Executable companion

The standard-library bundle is

harness/double_fibre_audit.py
harness/check_bundle.py
harness/double_fibre_certificate.json
harness/README.md

The audit executes finite witnesses and checks for the sealed declarations of §10.1, the required-output map of §10.2, the expected values of §10.3, and the covered extension tests, in ordinary and optimised Python, without bare assert statements, and emits a deterministic certificate. Its named checks include independently biting teeth and explicitly classified derived or shadowed coverage markers; the latter do not count as independent failure modes. The bundle gate checks inventory, hygiene, certificate equality, its own advertised counts, and scratch mutations that must be rejected by named markers.

Expected audit output:

double fibre audit passed: 64 checks

Expected bundle output:

bundle checks passed: 13 gates, 42 mutations

The executable audit establishes only the declared finite models. It does not certify any real verification pipeline, monitor deployment, or coordination system.

---

§11. Falsification surface

The framework is invalidated or its conclusion narrowed when any of the following occurs.

F1 - undeclared side channel. The verifier receives information not included in V. The relevant fibre and conditional entropy must be recomputed for the enlarged channel.

F2 - post-hoc comparison class. Histories, selectors, compatibility, prior, or target are changed after the verdict is known.

F3 - type mismatch. Compared selectors do not act on the same declared history type, or compared histories do not belong to the same visible skeleton class.

F4 - unsupported entropy claim. A pointwise conclusion is inferred from an average entropy bound without a target-fibre witness or pointwise premise.

F5 - hidden-pair/target conflation. Positive H(H, A∣V) is reported as positive H(Q∣V) without checking target constancy.

F6 - product assumption. The double fibre is counted as ℱ_O × 𝔄(D) without verifying compatibility.

F7 - inevitable contraction. Nested contraction is claimed without a fixed universe, restriction update, no-repair condition, and strictness witness.

F8 - enforcement by observation. A detector is said to enforce a property without complete mediation and pre-commit authority.

F9 - semantic overreach. A metadata monitor is said to certify semantic convergence beyond its declared predicate or probe contract.

F10 - agent necessity. A cognitive or heterogeneous agent is claimed necessary for enforcing a decidable prefix-closed safety invariant despite an available deterministic reference-monitor construction.

F11 - transaction/structure collapse. A transaction gate is treated as a structural viability predicate without an effect map and correspondence proof.

F12 - property-detection overclaim. Non-zero mutual information about a property is treated as full reconstruction, exact classification, or causal identification.

F13 - same-cycle feedback. Raw audit findings modify the producer while the original certification claim is kept unchanged. The revised object requires a new audit epoch.

F14 - envelope violation. A monitor claimed to be V-confined and sound in every compatible world commits prefixes outside the intersection 𝒮_∩ of Theorem 6.4 while the admissibility selector remains hidden. Then at least one of three holds: the soundness claim fails for some compatible selector; or the confinement claim fails, an undeclared selector channel being present - Remark 6.5 shows that a genuine selector channel legitimately escapes the envelope; or the declared proposal class is not selector-free, so the committed prefix carries selector information and the operative envelope is the one over 𝔄_{(v, p)}. The three are not exclusive. F1 applies to the enforcement layer in the second and third cases. Confinement must be stated as a claim under test rather than as a hypothesis: a monitor assumed V-confined cannot, by definition, be using a selector channel, and the second case would be unreachable.

---

§12. Open problems

1. Extend the finite theory to standard Borel spaces with regular conditional distributions and measurable selector families.
2. Extend the least-sufficient-refinement theorem (Theorem 3.8) beyond the finite case, and characterise when the abstract refinement V_Q is realisable by a physically implementable channel rather than a partition on paper.
3. Separate information-theoretic binding from computational hardness and query-limited boundary reconstruction.
4. Define sequential double binding under adaptive observations and changing selector families 𝔄_t(D).
5. Derive composition laws for coupled double fibres without assuming product compatibility.
6. Relate irreversible burden and capacity to continuation-set contraction under explicit repair and capacity-growth models.
7. Define intervention protocols that distinguish ranking, downstream veto, and generative-support exclusion.
8. Give a refinement theorem from abstract structural admissibility to an executable reference monitor.
9. Add liveness and recovery guarantees without weakening complete mediation.
10. Determine when bounded propagation lag plus projection conformance yields a quantitative bound on observable verdict divergence.
11. Formalise epoch semantics for audit feedback, selector revision, and re-certification.
12. Extend the sealed reference audit - now executable in the companion harness of §10.5 - with the side-channel and propagation-lag models of §10.4.

---

§13. Relation to the surrounding corpus

This paper composes, but does not collapse, several earlier lines.

• Domenoid of Admissibility supplies the non-trivial fibre of admissibility structures over one dynamic skeleton.
• The Physics of Abstraction supplies histories, seam-relative persistence, observation fibres, target factorisation, and lineage binding.
• Severance Defect and the Binding Functional supplies the distinction between functional severance and reconstructive binding, together with the confined-access non-absorption pattern.
• Identity Does Not Drift supplies the separation between budget wear and witness transport.
• Identifiability Bridge supplies the conditional distinction between property detection and full reconstruction.
• IIC v2.1 supplies a separate liveness coordinate.
• Subtle Substitution motivates the temporal contraction question.
• Verification Is Not Causal motivates channel isolation, corrected here to a precise confined-access statement.
• Transaction-Level Admissibility Stops Bad Actions. Structural Admissibility Stops Good-Looking Systems From Dying Slowly. supplies the action/effect pullback distinction.
• Continuity-Bounded Coordination: Why Multi-Agent Systems Still Drift supplies the propagation and cold-start implementation problem.
• The Structural Navigation Agent: Enforcement Architecture and Structural Analysis for Multi-Agent Coordination supplies the separation between detection and transition authority, corrected here to a deterministic reference-monitor core.
• Will as a Prior Constraint: Why the Prefrontal Cortex Exists at All supplies the motivation for constraining before a transition rather than correcting after it, which is the pre-commit discipline of §6.3. Its clinical case - consequences understood while the transition is no longer withheld - is an instance of detection without commit authority, the pattern F8 names. Its distinction between holding an impulse and extinguishing it corresponds, at the formal layer, to the gap between the 𝒮-monitor and the monitor that rejects everything: both are sound, and only the first leaves anything admissible.

The double fibre is the epistemic skeleton connecting these works. It is not a universal decomposition of engineered vitality. Directedness, phase, burden, memory, liveness, returnability, and coordination enter only through typed targets, hidden histories, selector families, or additional dynamics. They should not be promoted to new fibres without new forgetting maps.

---

Conclusion

Verification can fail in two structurally different ways before any algorithmic weakness appears.

The artifact may forget how it was produced. The skeleton may forget the rule under which that production should be judged. Their compatible joint inverse image is the double fibre.

A visible exact verdict exists precisely when the target is constant on that fibre. A single same-visible/different-target pair refutes exact verification. Conditional entropy measures how much of the hidden pair remains, but hidden-pair ambiguity must not be confused with ambiguity of the selected target. Post-processing cannot repair target ambiguity under confined access, while weaker property detection can remain possible under separate premises.

Meaning contraction is not smuggled into this theorem. It follows only from a declared restriction dynamics and can be absent, repaired, or reversed outside that class.

Finally, observation is not enforcement. A deterministic reference monitor can enforce a decidable prefix-closed safety property under complete mediation, while cognitive interpretation, semantic auditing, revision, liveness, and recovery remain separate obligations.

The resulting architecture is deliberately conservative:

declare the hidden completion → declare the visible channel → inspect the double fibres → test the target → separate verification from enforcement.

Anything stronger requires another premise, another witness, or another theorem.

---

References

Corpus

Barziankou, M. (2026). Navigational Cybernetics 2.5 - Axiomatic Core, Version 2.1. The Urgrund Laboratory, PETRONUS. DOI: 10.17605/OSF.IO/NHTC5.

Barziankou, M. (2026). Severance Defect and the Binding Functional: Observation-Relative Non-Reconstructibility and the Impossibility of Uniform Exact Absorption under Confined Markov Access. Publication pair DOI: 10.17605/OSF.IO/5VJMR.

Barziankou, M. (2026). Operator over Dynamics - A Traceable Structural Program (2025-2026) - and Its Formal Core - the Domenoid of Admissibility. DOI: 10.17605/OSF.IO/3ESN4.

Barziankou, M. (2026). Identifiability Bridge - Conditional Admissibility Theorems for Property Detection under Non-Reconstructibility within Navigational Cybernetics 2.5. DOI: 10.17605/OSF.IO/3F6UJ.

Barziankou, M. (2026). IIC v2.1 - A Class-Relative Structural Law of Adaptive Behaviour as a Conditional Theorem over Navigational Cybernetics 2.5. DOI: 10.17605/OSF.IO/NYT45.

Barziankou, M. (2026). ONTOΣ XIV - Nested Substrates and the Frame-Relative Derivative, with Cross-Layer Forgetful Separation: A Categorical Foundation. Bundle DOI: 10.17605/OSF.IO/KAGMH.

Barziankou, M. (2026). ONTOΣ XV - Spin-Channel and Nestability, with its formal companion. Bundle DOI: 10.17605/OSF.IO/EAUD5.

Barziankou, M. (2026). The Physics of Abstraction: Identity at the Seam. DOI: 10.17605/OSF.IO/QJ5BR.

Barziankou, M. (2026). Identity Does Not Drift: Channel Switching, the Two Ledgers, and the Parallel Tunnel. DOI: 10.17605/OSF.IO/4NMTW.

Barziankou, M. (2026). Will as a Prior Constraint: Why the Prefrontal Cortex Exists at All. DOI: 10.6084/m9.figshare.31288699.

Barziankou, M. (2025-2026). Verification Is Not Causal · Subtle Substitution · Transaction-Level Admissibility Stops Bad Actions. Structural Admissibility Stops Good-Looking Systems From Dying Slowly. · Continuity-Bounded Coordination: Why Multi-Agent Systems Still Drift · The Structural Navigation Agent. Local corpus editions; cited in §13 for architectural lineage.

General

Alpern, B., and Schneider, F. B. (1985). Defining Liveness. Information Processing Letters 21(4), 181-185. (Safety/liveness boundary used in §6.3.)

Anderson, J. P. (1972). Computer Security Technology Planning Study. ESD-TR-73-51, U.S. Air Force Electronic Systems Division. (The reference-monitor concept behind Theorem 6.2.)

Cover, T. M., and Thomas, J. A. (2006). Elements of Information Theory, 2nd ed. Wiley. (Conditional entropy, chain rule, data-processing inequality, Fano's inequality - §§3, 4, 8.)

Ramadge, P. J., and Wonham, W. M. (1987). Supervisory Control of a Class of Discrete Event Processes. SIAM Journal on Control and Optimization 25(1), 206-230. (The maximal-permissiveness pattern of Proposition 6.3.)

Schneider, F. B. (2000). Enforceable Security Policies. ACM Transactions on Information and System Security 3(1), 30-50. (Execution-monitoring enforceability of prefix-closed safety - §6.3.)

---

Companion code

The deterministic companion verifier and reproducibility harness are available in the public repository: The Double Fibre of Verification.

Originally published at https://petronus.eu.

SHA-256: 8c8fc8943e9d34ec3bd49b8377e73e0aa37912a376113ca4b9f40e8204178db3

---

NC2.5 · Urgrund · MxBv · PETRONUS · [e-mail] · CC BY-NC-ND
Originally published https://medium.com/@MxBv/the-double-fibre-of-verification-68a67ef63e3f