Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original Single-Terminal Ternary Obstruction

Abstract

The complete original causal leaf law places every joint ternary postprocessing in a common closed score halfspace.

Theorem 1.1 (Complete records obey the ternary score obstruction).

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/OriginalSingleTerminalTernaryObstruction.complete_original_single_terminal_ternary_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

Source retains 0<d<1, sin(2 theta) nonzero, the same installed unitary N with nonzero commutator with the xi projector, and the original V0=U exp(i theta W), V1=V0 W, W=I-2ff*, q=(xi+e)/sqrt(2), E=qq*. The sole installed preparation is the rank-one density of sqrt(d)Uq+i sqrt(1-d)Uf. The rectangular isometry B and Kb B=B Vb/sqrt(2) retain the five-dimensional source correspondence as premises.

A CausalTree is a finite complete tree. A control node applies the same N, an instrument node retains both original J outcomes with branch Ad(Vb)/2, and a stop node performs the original two-cell terminal exactly once and stops. Leaves are never identified by their marks: their complete chronological words, action positions, labels, mismatch marks and timeout marks remain distinct. Empty words, no-control trees, no-instrument trees and unequal depths are included. There is no successor operation after the terminal.

fixedStoppingTree embeds every finite fixed action string, checkpoint function and past-label stopping table. Continuing uses the same remaining string, while the end is forced. The universal causal tree domain also permits the larger mathematical comparison in which the next action depends on the past. This comparison does not install label-dependent action choice.

Induction on the actual branch evaluation gives the entire substate alpha(w) Uw X Uw*, with alpha(w)=2 to the negative number of J calls. Tree induction gives positive weights with sum one. These weights depend only on the actual tree word, never on X. Trace cyclicity then gives both terminal cells alpha(l) Tr(Rl X) and alpha(l) Tr((I-Rl) X), where Rl=Uw* E Uw. No zero terminal probability is removed or divided by, and both cells together have mass alpha(l).

The lifted control is B N B*+(I-BB*). Multiplying the original intertwiners along each actual word gives the same leaf substate on inputs B X B*. Pulling back the lifted terminal by B gives exactly E or I-E. The resulting equality is confined to this code sector; it makes no claim for arbitrary five-dimensional inputs.

Stochastic t is one joint kernel c(l,b,a), nonnegative and summing to one over the three a labels at each complete record (l,b). Its effects are the sum over actual leaves of alpha(l)[c(l,1,a)Rl+c(l,0,a)(I-Rl)]. The theorem derives the Born pairing for every mathematical input matrix and proves positive normalized output distributions for every density input. The stochastic kernel and convex hull are mathematical outer comparisons; they grant neither an external coin nor independent choice of simulators or mixing weights.

RankOneContext 3 is the existing algebraic carrier for a complete normalized rank-one projective basis. PureStateHandshake supplies the terminal rank-one sandwich. Born positivity bounds every basis overlap between zero and one. Each of the two terminal cells contributes at most one to the sum of the three correct responses, so each actual leaf contributes at most two. The derived weights sum to one, yielding score at most 2/3.

BasisObstruction states this score bound, maximum operator distance at least 1/3, and a mathematical basis-state witness. The witness output is a nonnegative three-label distribution of mass one whose total variation from the ideal point mass is at least 1/3. The singleton event gives the TV bound through TotalVariation.Metric.total_variation_eq_sup_event_gap. These basis states are separation witnesses, not installed preparations.

The matrix norm is explicitly Mathlib’s Hilbert-L2 operator norm: it equals the continuous-linear-map norm of toEuclideanCLM. maxDistance is the maximum of the three individual matrix distances and is proved equal to the finite-product norm. The score is continuous and real linear in this topology. Its 2/3 halfspace and the set of POVMs are closed and convex. Their intersection contains the operational image, hence its convex hull and closure. The same score, distance and normalized TV conclusions follow throughout that closure.

Three separately approximated binary effects do not define one joint ternary POVM. Probability effects do not determine successor instruments. The result concerns the original single terminal and classical postprocessing, with no reset, copy, inverse gate, extra effect, coherent label access, postselection, unread branch or postterminal quantum continuation.

References