Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

FiniteEdgeProbeCorrespondence

Abstract

Loop-corrected labelled endpoint probes identify graph connectivity with actual Hilbert components.

Let V be a finite coordinate type, E an arbitrary edge-label type, and u and v its endpoint maps. The probe indices are the disjoint sum of V and E. A vertex a contributes its coordinate basis vector. An edge with equal endpoints contributes that same basis vector; an edge with distinct endpoints contributes the sum of its two basis vectors divided by the square root of two. The anchor of a vertex is itself and the anchor of an edge is its first endpoint. No labels are identified: repeated edges, reverse-labelled edges and loops are separate indices. Vertices without incident edges remain basis probes, and the construction includes an empty edge family. Even an empty V is permitted when the endpoint maps exist.

Theorem 1.1 (Normalized spanning probes and exact components).

Lean statement: D5/S3/Quantum/Reduction/FiniteEdgeProbeCorrespondence.construction

Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/FiniteEdgeProbeCorrespondence.construction (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite V with decidable equality, every type E and endpoint maps u and v, all the explicit probes have squared norm one and their complex linear span is the entire coordinate space. For any two probe indices, the equivalence closure of their nonzero inner products holds if and only if their anchors are connected by the equivalence closure of the original endpoint generators. For every probe index j, the actual hilbertComponent of its quotient class is exactly the coordinate subspace on the vertices connected to its anchor. Its complex finrank is the cardinality of that vertex subtype.

Each nonzero coordinate of a probe lies in the graph class of its anchor. A nonzero inner product has a nonzero summand, hence a shared coordinate; this proves one implication of the component correspondence. Conversely, each original edge gives a path from its first endpoint basis probe through its labelled edge probe to its second endpoint basis probe. Every edge probe is linked to its anchor, so this proves the other implication. For the subspace equality, each component probe vanishes outside the graph class, while every basis vector in that class belongs to the actual probe component. The coordinate basis restricted to that class is linearly independent, yielding the exact dimension. The number of labelled configurations is not used as a dimension.

Theorem 1.2 (Endpoint closure under a change of carrier).

Lean statement: D5/S3/Quantum/Reduction/FiniteEdgeProbeCorrespondence.restricted_endpoint_closure

Proof. Machine-checked in Lean as D5/S3/Quantum/Reduction/FiniteEdgeProbeCorrespondence.restricted_endpoint_closure (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any ambient type A, subset S, edge-label type E, maps u and v into S, and a and b in S, connectivity generated by the lifted endpoints in S is equivalent to connectivity generated by their values in A. There is no finiteness or nonemptiness assumption. Mapping a subtype path to values gives the forward direction. For the reverse direction, a is a fallback value defining a retraction from A onto S. It fixes every endpoint and transports each generator and each equivalence-closure constructor back to S.

For the actual FIB support, take V to be ActiveVertex(c), E to be Fin(3t-3), and the lifted endpoints to be the two values of chosenPair(c,e), together with their endpoint activity proofs. The ambient generator says that chosenPair(c,e) equals the ordered endpoint pair. Product extensionality identifies it with the two endpoint equations in Connected. The restriction theorem therefore identifies the lifted generated equivalence with supportSetoid(c) on subtype values, which is activeSetoid(c). This correspondence is derived from chosenPair; it is not a definitional equality between the two generated relations. When t is at least two, 3t is nonzero, so the ambient residue type is finite and its active subtype is finite. The label zero exists because 3t-3 is positive, and its first endpoint supplies an active vertex, proving nonemptiness. Balanced is unnecessary for this construction; it enters only further consequences such as the existing at-most-two active component bound.

Apply exact_component_port_dimension to the explicit normalized spanning menu. In its existing flagged coherent-port model, the minimum coherent dimension is the maximum of the actual component dimensions, now identified with component vertex counts. The lower bound retains probability preservation for every original probe and every density input. Apply probe_channel_block_form only under its trace-preserving Kraus identity and the same universal probability preservation. Its cross-component terms retain the actual environment Gram coefficients; they need not vanish. Pinching is the composite of the particular constructed port. The abstract decomposition and graph-algebra background is consistent with Ortiz and Paulsen, arXiv:1412.7101v1, Theorem 3.2, and the nondisturbance background with Barnum, Hayden, Jozsa and Winter, quant-ph/0011072v2, Lemma 1. These references do not supply the explicit Lean endpoint correspondence. The native state, observer, preparation and instrument interpretation remains an additional bridge; this coordinate construction does not assert a physical realization, a QFT model or an identification of native physical constants.

The following is an ordinary finite-dimensional application, outside the two Lean Describe claims above. Fix a natural t ≥ 2 and c : Choices(t) with Balanced(c). Use precisely V = ActiveVertex(c), E = Fin(3t − 3), and the activity-certified endpoints uₑ, vₑ of chosenPair(c,e). Let Hsys = ℂ^V with its coordinate inner product, and Pᵢ = |i⟩⟨i|. The actual activeSetoid(c) classes C partition V. The native support inputs used below are that each such class is closed under the directed chosen edges, is strongly connected and contains an actual label; the ordered chosen endpoints determine their original label, and label zero is nonloop. These are ordinary native support consequences of the six formPair ranges and integer balance, not additional conclusions of construction or restricted_endpoint_closure. The native source is Feldman, The Missing Zigzag, arXiv:2609.26114v1, §5, equation (2) and the balance-only setting of Definition 5.1. The component correspondence proved above identifies the coordinate carrier; it does not choose a physical dynamics.

Keep the entire original probe index V ⊕ E. A loop uses its one coordinate vector, and a nonloop uses (|uₑ⟩ + |vₑ⟩)/√2, exactly as in probes above. Write Pₛ for each resulting rank-one projection. Each {Pₛ, I − Pₛ} is a separate binary measurement setting; the unweighted collection of all Pₛ is not one POVM. Every density below ranges over all complex positive semidefinite trace-one matrices on the original Hsys, including coherent inputs across different components. A system effect X means any operator with 0 ≤ X ≤ I on that same Hsys. No stationarity or diagonal-input restriction replaces these quantifiers. Equal probe vectors, reverse indices and loops do not merge or manufacture original labels.

Assign a fixed finite real cost εₑ to each original label and a real T > 0. Put wₑ = exp(−εₑ/T) > 0 and use the source-row convention Wᵢⱼ = ∑_{e:uₑ=i,vₑ=j} wₑ. In each actual closed component choose its positive Perron data rᶜ and λ_C with W_C rᶜ = λ_C rᶜ. The parameter map to D5/S3/Combinatorics/Graph/Pressure/WeightedWalks is its finite type X = C, edge(i,j) meaning an actual chosen label i → j, and pair cost equal to εₑ for that unique native label; off-support costs are immaterial. The support inputs provide Network.connected and Network.hasEdge, and native endpoint injectivity makes its Prop-valued W equal to this original-label sum. For a general labelled graph the sum must still be retained, rather than selecting one representative cost. The existing unrestricted_walk_laws supplies (W_Cⁿ1)ᵢ and startwise growth log λ_C, including periodic support. The stationary Doob/KL consequence already explained in that owner and D5/S3/Combinatorics/Graph/Pressure/CyclePressure apply with the same fixed costs and actual support; cycle_pressure_laws gives m_C − T log d_C ≤ −T log λ_C ≤ m_C and the right zero-temperature limit m_C. No pressure or Perron theorem is added here. Different closed components may have different λ_C; the following construction normalizes each separately. A single global dual eigenvalue would require their roots to agree.

To see the convention at the quantum interface, set Aₑ = √wₑ |vₑ⟩⟨uₑ| and ℒ(Z) = ∑ₑ Aₑ Z Aₑ†. For any coordinate columns p and f, direct multiplication gives ℒ(diag p) = diag(Wᵀp) and ℒ*(diag f) = diag(Wf). Thus H_C = diag(rᶜ) is a positive dual eigenmatrix, not a state eigenmatrix. With G_C = H_C^(1/2), the label in C has Kₑ = λ_C^(−1/2) G_C Aₑ G_C^(−1) = √qₑ |vₑ⟩⟨uₑ|, where qₑ = wₑ rᶜ(vₑ)/(λ_C rᶜ(uₑ)) > 0. Its source sum is ∑_{e:uₑ=i}qₑ = (W_C rᶜ)ᵢ/(λ_C rᶜ(i)) = 1. Consequently ∑ₑ Kₑ†Kₑ = ∑ᵢ Pᵢ = I on the whole original carrier, with every original label nonzero. The unnormalized ℒ is CP but need not be trace nonincreasing. The complete K family defines the chosen instrument; neither a physical temperature nor native transition dynamics is inferred from these coordinates.

The operational premises for the original branch e are its CP property, source effect qₑPᵤₑ and one-dimensional output support span(vₑ). Here 0 < qₑ ≤ 1, so the effect is nonzero and rank one. Heinosaari and Wolf, arXiv:1005.5659v2, Proposition 8, applies exactly to a CP map with this effect: it has the form 𝓘ₑ(ρ) = Tr(ρ qₑPᵤₑ) τₑ for a density τₑ. The target-support premise forces τₑ = Pᵥₑ, since a positive trace-one operator on that line is its unit projection. By complex linearity the resulting branch identity is 𝓘ₑ(Z) = qₑ Zᵤₑᵤₑ Pᵥₑ = Kₑ Z Kₑ† for every matrix Z. Thus these premises fix the CP branch maps, while Kraus decompositions and coherent dilations remain nonunique. Removing target support permits other output densities in Proposition 8. Let Φ = ∑ₑ 𝓘ₑ and Qᵢⱼ = ∑_{e:i→j}qₑ; then Φ(Z) = diag(Qᵀ diag Z), so this particular system channel discards input off-diagonal entries.

Now retain an orthogonal record space ℰ = ℂ^E with basis |e⟩ indexed by the actual original labels, and choose the coherent isometry 𝒱x = ∑ₑ Kₑx ⊗ |e⟩ from Hsys to Hsys ⊗ ℰ. Its adjoint Gram is 𝒱†𝒱 = ∑ₑ Kₑ†Kₑ = I. Define Δ(B) = ∑ₑ |e⟩⟨e| B |e⟩⟨e|, Jcoh(ρ) = 𝒱ρ𝒱†, and Jcl(ρ) = (id ⊗ Δ)(Jcoh(ρ)). Thus Jcl(ρ) = ∑ₑ KₑρKₑ† ⊗ |e⟩⟨e|, whereas Jcoh retains the terms KₑρK_f† ⊗ |e⟩⟨f| for e ≠ f. These are two record outputs for the same instrument and its same original labelled branches, with no change to qₑ, Kₑ or Φ.

The available observation algebra is B(Hsys) ⊗ Diag(ℰ), whose elements are ∑ₑ Xₑ ⊗ |e⟩⟨e|. For every original input density ρ, every label e and every system effect X, expansion of either output gives Tr[(X ⊗ |e⟩⟨e|) Jcoh(ρ)] = Tr[(X ⊗ |e⟩⟨e|) Jcl(ρ)] = Tr[X KₑρKₑ†] = qₑ ρᵤₑᵤₑ ⟨vₑ|X|vₑ⟩. The record diagonal projection selects precisely e on both sides. Taking X = I gives the same branch probability; summing over e gives the same system marginal Tr_ℰ Jcoh(ρ) = Tr_ℰ Jcl(ρ) = Φ(ρ). Linearity gives equality for the entire stated observation algebra, in particular for every original probe on every original branch, including its complementary binary outcome. This is equality between two outputs. It does not say Tr[PₛΦ(ρ)] = Tr[Pₛρ]. Record-off-diagonal joint effects are additional observations.

The retained coherence has an explicit native witness. For every actual active coordinate i put ηᵢ = 𝒱|i⟩ = ∑{e:uₑ=i}√qₑ |vₑ,e⟩, where |v,e⟩ = |v⟩ ⊗ |e⟩. Distinct labels give orthogonal terms, so ‖ηᵢ‖² = ∑{e:uₑ=i}qₑ = 1. For i ≠ j the outgoing label sets are disjoint because an original label has one source. Hence ⟨ηᵢ,ηⱼ⟩ = 0 even when some target vertices coincide. The nonloop zero label supplies actual distinct active coordinates i,j; no extra vertices or reverse labels are needed. Let ψ± = (|i⟩ ± |j⟩)/√2 and ρ± = |ψ±⟩⟨ψ±|. They are distinct orthogonal pure input states with identical coordinate diagonals.

On these two inputs Jcl has the identical value ½∑{e:uₑ=i or uₑ=j}qₑ |vₑ,e⟩⟨vₑ,e|, because each rank-one branch uses only the source diagonal. In contrast Jcoh(ρ±) is the pure projection onto Ω± = (ηᵢ ± ηⱼ)/√2. The orthonormality just proved gives ‖Ω±‖ = 1 and ⟨Ω+,Ω−⟩ = 0. Thus the coherent outputs remain orthogonal. The genuine joint effect M = |Ω+⟩⟨Ω+| has coherent probability one on ρ+. For every outgoing e of i or j, |⟨Ω+|vₑ,e⟩|² = qₑ/2. Multiplying by the dephased branch mass qₑ/2 and summing proves Tr[M Jcl(ρ+)] = (∑{e:uₑ=i}qₑ² + ∑_{e:uₑ=j}qₑ²)/4 ≤ 1/2: each sum of squares is at most the square of its source sum, namely one. This M couples different record labels and lies outside B(Hsys) ⊗ Diag(ℰ); the branch/system equality has not licensed its measurement.

Full joint access permits recovery by one decoder defined on the entire enlarged output, not just on the generated image. Write Pcode = 𝒱𝒱† and choose any fixed input density τ. Define D(Y) = 𝒱†Y𝒱 + Tr[(I − Pcode)Y]τ for every operator Y on Hsys ⊗ ℰ. To verify CP and trace preservation, diagonalize τ = ∑ₐ tₐ|a⟩⟨a| and take an orthonormal basis |b⟩ of the complement of ran(𝒱). Kraus operators for D are 𝒱† and √tₐ|a⟩⟨b|; their adjoint Grams sum to Pcode + (∑ₐtₐ)(I − Pcode) = I. Their branch sum is exactly the displayed D. The complement term vanishes on 𝒱ρ𝒱†, and 𝒱†𝒱 = I gives D(Jcoh(ρ)) = ρ for every original density. Conversely a decoder on Jcl that recovered every original density would have to send its identical outputs on ρ+ and ρ− to two different states, which no map can do. Therefore the stated observation algebra fails to determine universal quantum recoverability even for this one native labelled instrument. This does not exclude recovery on a separately restricted input family or after an additional operation.

For a literal instance take t = 2 and forms III, IV, VI at classes k = 2,3,4, respectively. The actual labels e = 0,1,2 give chosenPair endpoints 5 → 2, 2 → 3, 3 → 5 in ZMod 6. Each active vertex has one incoming and one outgoing label, so this c is Balanced. In coordinate order (5,2,3), W = [[0,1,0],[0,0,1],[1,0,0]] for zero costs, r = (1,1,1), λ_C = 1 and every qₑ = 1. The actual Kraus operators are K₀ = |2⟩⟨5|, K₁ = |3⟩⟨2| and K₂ = |5⟩⟨3|. These chosen edges form one active component of size three. They are a chosen-support cycle, not an asserted closed native pitch history: the source step sum is 5 + 2 + 3 = 10 = 4 modulo 6, so the separate closed-pitch constraint is not met.

For s = (|5⟩ + |2⟩ + |3⟩)/√3, its coherent recorded image is Ω = (|2,0⟩ + |3,1⟩ + |5,2⟩)/√3. Thus Jcoh(|s⟩⟨s|) = |Ω⟩⟨Ω| and Jcl(|s⟩⟨s|) = (|2,0⟩⟨2,0| + |3,1⟩⟨3,1| + |5,2⟩⟨5,2|)/3. The joint projection |Ω⟩⟨Ω| has probabilities one and 1/3. Both system marginals are I₃/3. Each of the three original vertex projections and three original edge projections has trace one, so all six system yes probabilities are 1/3 in both outputs. The three edge probes on the input |s⟩ instead have probability 2/3, displaying explicitly the difference between matched output observations and input-probability preservation. Comparing the unitary permutation ∑ₑKₑ with its measured lift would give different edge-probe outputs on this input; the present comparison fixes the same rank-one instrument and system marginal throughout.

For a specified finite n, use a fresh orthogonal ℰ record at each step and apply the same 𝒱 only to the current system. Retain the earlier records without coupling them back to that system. Repeated expansion gives 𝒱⁽ⁿ⁾x = ∑_{ω=(e₁,…,eₙ)} K_ωx ⊗ |ω⟩, with K_ω = Kₑₙ⋯Kₑ₁ and |ω⟩ the ordered tensor record; incompatible strings have zero K_ω. At n = 0 this is the identity with the single empty string. Dephasing all fresh records keeps exactly K_ωρK_ω† ⊗ |ω⟩⟨ω|. Sequentially measuring those same labels gives the identical branch product, by composition of the same CP maps. Thus for every original density, every full original label string and every final system effect X, both protocols have branch expectation Tr[X K_ωρK_ω†] at every finite n. This is a finite iteration of the same-instrument equality. Coherent record reuse, erasure, or record-to-system feedback is an additional operation and need not preserve it. The explicit retained carrier is Hsys ⊗ ℰ^⊗n, with its order and finite length supplied; no indefinitely growing archive fits a fixed carrier by this construction.

The orthogonal-edge record, record dephasing and product-of-branches mechanisms are the existing suppliers in Recursive relational observation: minimal pure records for the five-mode dilation, docs/develop/theory/RECURSIVE_RELATIONAL_OBSERVATION_MINIMAL_RECORD_DILATIONS.md, §§1, 4–6. Its stipulated source is a square with a leaf, positive loops, H = ℂ⁵ ⊗ ℂ², internal Pauli transports and distinct read/feedback contracts. Its smaller unlabelled realization has a different unread channel; its conditional unitary-flag correction requires the actual flag measurement and permitted inverse controls. Those constructions and minima are not repeated or identified with chosenPair here. The application above supplies the actual native parameter map and equalities for the SAME original label instrument, together with a joint-effect and recoverability separation that the declared system/classical-label observations cannot see.

The homogeneous Perron instrument also differs from a fixed-horizon Boltzmann tilt. On the whole original carrier, for a specified N ≥ 1 and terminal boundary H_N = I, put H_k = ℒ*(H_{k+1}) = diag(W^(N−k)1), G_k = H_k^(1/2), and Kₑ,k = G_{k+1}AₑG_k^(−1). Every native source has a positive outgoing label, so these H_k are positive definite. Direct substitution gives ∑ₑ Kₑ,k†Kₑ,k = G_k^(−1)ℒ*(H_{k+1})G_k^(−1) = I. Adjacent inverse roots cancel in chronological path products, giving K_ω = A_ωG₀^(−1) because G_N = I. For each original density ρ, r_N = Tr(H₀ρ) > 0 and σ₀ = G₀ρG₀/r_N therefore give K_ωσ₀K_ω† = A_ωρA_ω†/r_N. Nonzero normalized terminal branches agree, but the initial filter changes a general ρ. For basis input Pᵢ the filter leaves Pᵢ unchanged and each compatible labelled path has probability (∏wₑ)/(W^N1)ᵢ. The homogeneous Perron path law within C is instead (∏wₑ)rᶜ(end)/(λ_C^N rᶜ(i)). Fixing both endpoints makes their conditional path weights proportional to the same product when the event has positive mass; fixing only the start does not remove the differing terminal factor.

Restricting this comparison to one component and replacing its terminal I by H_C gives H_k = λ_C^(N−k)H_C and the homogeneous Kₑ, but the terminal branch for a density ρ on that component then retains G_C A_ωρA_ω†G_C/Tr(H₀ρ), rather than the terminal-I state. These boundaries cannot be exchanged silently. On other supports a singular H_k would require its support inverse; the transformed family is complete only on supp(H_k), zero-weight inputs are excluded, and completion on the ambient complement is extra data. The native positive-outgoing setting above avoids that singular case. These are finite-boundary comparisons of the chosen coordinate maps, not a long-time mixing or native history assertion.

For eventual detection reuse D5/S3/Quantum/Measurement/EventualClickDoobInstrument under its own exact conditions: repeat one finite-dimensional complete instrument with no-click Kraus Qₐ and click Kraus Lₓᵦ, so ∑ₐQₐ†Qₐ + ∑ₓ,ᵦLₓᵦ†Lₓᵦ = I, and use the ACTUAL survival limit F = limₙ(N*)ⁿ(I), where N(Z) = ∑ₐQₐZQₐ†. Put R = I − F, P = supp(R), G = √R and Gplus its support inverse. The existing eventual_click_doob_instrument gives Qtildeₐ = GQₐGplus and Ltildeₓᵦ = LₓᵦGplus, completeness on P, and the intertwinings Ntilde(GZG) = GN(Z)G and Ctildeₓ(GZG) = Cₓ(Z) for every matrix Z. Consequently for every original density ρ with r = Tr(ρR) > 0, n ≥ 1 and click outcome x, Ctildeₓ Ntilde^(n−1)(GρG/r) = Cₓ N^(n−1)(ρ)/r; nonzero normalized terminal states coincide. There is no extra G on the click output and no requirement that the original ρ already lie in P. A balance-equation solution alone cannot replace the survival-limit premise. The support identity P Qₐ(I − P) = 0 does not assert (I − P)QₐP = 0 or that click outputs lie in P.

In particular D5/S3/Quantum/Measurement/NonProjectiveDarkEffect already supplies the two-state non-projective survival example; with its parameter a = 1 − p, its old |0⟩ renamed |b⟩ and old |1⟩ renamed |a⟩, its residual is p|a⟩⟨a| for 0 < p < 1. It is not a new native example. A complete Perron K family has total effect I, whereas the transformed eventual no-click subfamily has total effect P minus the transformed click effect and is incomplete whenever the latter is nonzero. Naming H_C a Perron matrix does not identify it with an eventual-event residual. Finite-horizon filtering, the complete homogeneous instrument, and conditioning on the actual eventual-click event retain their distinct boundary data. None of their conditional terminal-state equalities asserts all-input probe preservation on the original unfiltered input.

The coherent recoverability conclusion counts a phase reference fixing the relative record phases, coherent preparation and retention of ℰ, full joint access to Hsys ⊗ ℰ, the joint effect M and a permitted implementation of the entire-output decoder D. The dephased output supplies classical labels but not these coherent controls. Even for the displayed t = 2 instance, the proposed output carrier has dimension 3 × 3 = 9, with a three-dimensional code image; calling the label register a record does not make it a free classical flag before dephasing. Every input-dependent quantum carrier reaching the decoder must be counted. Therefore this enlarged-output recovery does not bypass exact_component_port_dimension in its specified flagged model, and neither matched marginals nor this construction settles the fixed M₅ all-lifts memory target. It supplies no map identifying this Zigzag chosen support with the one-bit no11 five-window kernel, the five-mode square-and-leaf model, or a closed-pitch-history law.

The chosen finite coordinate instrument and ordinary application establish the stated observer-relative distinction. Native preparations covering every original density, availability of the original binary settings, readable labelled branches with the specified source effects and target supports, the cost and temperature interpretation, phase-compatible joint operations and physical realization each remain additional bridges. No novelty, native physical dynamics, QFT realization or physical constant identification follows, and the ordinary calculations in this application are not newly Lean-certified statements.

References