Rendezvous vector systems

Abstract

A quantitative gap for symmetric rendezvous vector systems.

Definition 1.1 (Hypercube vertices).

$$\forall d\in \mathbb{N},RendezvousVectorSystemGap.Vertex\left(d\right)=\mathrm{Finset}\left(\mathrm{Fin}\left(d\right)\right)$$

Formalization. D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Vertex (✓ std3).

Citation. C. Wang (2026). Quantum-assisted rendezvous on hypercubes: a quantum Bernoulli noise approach. URL: https://arxiv.org/abs/2610.12949v1.

Commentary.

A vertex is a finite subset of Fin d, as in Wang’s hypercube model in §2. WindowSeamCodes.Word is this finite-set type.

Definition 1.2 (Fixed-cardinality outputs).

$$\forall d\in \mathbb{N},\forall t\in \mathbb{N},RendezvousVectorSystemGap.Output\left(d,t\right)=\{(A:\mathrm{Finset}\left(\mathrm{Fin}\left(d\right)\right))//Finset.card\left(A\right)=t\}$$

Formalization. D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Output (✓ std3).

Citation. C. Wang (2026). Quantum-assisted rendezvous on hypercubes: a quantum Bernoulli noise approach. URL: https://arxiv.org/abs/2610.12949v1.

Commentary.

An output is a t-element subset of Fin d. Erdos7.CommonTreeUnion.Choice is the subtype with this cardinality equation. These are the output sets in §2.

Definition 1.3 (The rendezvous condition).

$$\forall d\in \mathbb{N},\forall t\in \mathbb{N},\forall sigma\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall tau\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall A\in RendezvousVectorSystemGap.Output\left(d,t\right),\forall B\in RendezvousVectorSystemGap.Output\left(d,t\right),(RendezvousVectorSystemGap.Wins\left(sigma,tau,A,B\right))\iff ((\mathrm{Disjoint}\left(Subtype.val\left(A\right),Subtype.val\left(B\right)\right))\wedge ((Subtype.val\left(A\right))\cup (Subtype.val\left(B\right))=\mathrm{symmDiff}\left(sigma,tau\right)))$$

Formalization. D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Wins (✓ std3).

Citation. C. Wang (2026). Quantum-assisted rendezvous on hypercubes: a quantum Bernoulli noise approach. URL: https://arxiv.org/abs/2610.12949v1.

Commentary.

Equation (2.5) requires the two output sets to be disjoint and their union to equal the symmetric difference of the starting vertices.

Definition 1.4 (Number of outputs as a real number).

$$\forall d\in \mathbb{N},\forall t\in \mathbb{N},RendezvousVectorSystemGap.n\left(d,t\right)=(Nat.cast\left(Nat.choose\left(d,t\right)\right):\mathbb{R})$$

Formalization. D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.n (✓ std3).

Source. Repository-derived.

Commentary.

The binomial coefficient counts the outputs. Its value here is cast from the natural numbers to the real numbers.

Definition 1.5 (The quantitative gap).

$$\forall d\in \mathbb{N},\forall t\in \mathbb{N},RendezvousVectorSystemGap.kappa\left(d,t\right)=\frac{1}{(RendezvousVectorSystemGap.n\left(d,t\right){)}^4\cdot (4\cdot Real.sqrt\left(2\right)\cdot (Nat.cast\left(t\right):\mathbb{R})+2{)}^2}$$

Formalization. D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.kappa (✓ std3).

Source. Repository-derived.

Commentary.

The gap depends on the number of outputs and the step length. It is positive whenever the number of outputs is positive.

Theorem 1.6 (A dimension-independent vector bound).

$$\forall V\in Type\ast ,\forall ag\in \mathrm{AddCommGroup}\left(V\right),\forall module\in \mathrm{Module}\left(\mathbb{R},V\right),\forall C\in PreInnerProductSpace.Core\left(\mathbb{R},V,Real.instRCLike,ag,module\right),\forall d\in \mathbb{N},\forall t\in \mathbb{N},(2\le t)\Rightarrow ((2\cdot t<d)\Rightarrow (\forall h\in V,\forall u\in RendezvousVectorSystemGap.Vertex\left(d\right)\to \left(RendezvousVectorSystemGap.Output\left(d,t\right)\to V\right),\forall v\in RendezvousVectorSystemGap.Vertex\left(d\right)\to \left(RendezvousVectorSystemGap.Output\left(d,t\right)\to V\right),\forall delta\in \mathbb{R},(0\le delta)\Rightarrow ((delta\le 1)\Rightarrow ((Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),h,h\right)=RendezvousVectorSystemGap.n\left(d,t\right))\Rightarrow ((\forall sigma\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall A\in RendezvousVectorSystemGap.Output\left(d,t\right),Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),h,u\left(sigma,A\right)\right)=1)\Rightarrow ((\forall tau\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall B\in RendezvousVectorSystemGap.Output\left(d,t\right),Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),h,v\left(tau,B\right)\right)=1)\Rightarrow ((\forall sigma\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall A\in RendezvousVectorSystemGap.Output\left(d,t\right),Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),u\left(sigma,A\right),u\left(sigma,A\right)\right)\le 1)\Rightarrow ((\forall tau\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall B\in RendezvousVectorSystemGap.Output\left(d,t\right),Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),v\left(tau,B\right),v\left(tau,B\right)\right)\le 1)\Rightarrow ((\forall sigma\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall A\in RendezvousVectorSystemGap.Output\left(d,t\right),\forall Aprime\in RendezvousVectorSystemGap.Output\left(d,t\right),(A\ne Aprime)\Rightarrow (Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),u\left(sigma,A\right)+u\left(sigma,Aprime\right),u\left(sigma,A\right)+u\left(sigma,Aprime\right)\right)\le 2))\Rightarrow ((\forall sigma\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall tau\in RendezvousVectorSystemGap.Vertex\left(d\right),\forall A\in RendezvousVectorSystemGap.Output\left(d,t\right),\forall B\in RendezvousVectorSystemGap.Output\left(d,t\right),(RendezvousVectorSystemGap.Wins\left(sigma,tau,A,B\right))\Rightarrow (Inner.inner\left(\mathbb{R},V,PreInnerProductSpace.Core.toInner\left(\mathbb{R},V,Real.instRCLike,ag,module,C\right),u\left(sigma,A\right),v\left(tau,B\right)\right)=1-delta))\Rightarrow (RendezvousVectorSystemGap.kappa\left(d,t\right)\le delta)))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.vector_system_gap (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. C. Wang (2026). Quantum-assisted rendezvous on hypercubes: a quantum Bernoulli noise approach. URL: https://arxiv.org/abs/2610.12949v1.

Commentary.

Consider a real vector space with a positive semidefinite inner-product core. The two vector families have unit pairing with h, squared lengths at most one, and a two-outcome squared-length bound for the first family. Every winning pair has pairing 1 − delta. For t at least two and d greater than twice t, delta is at least kappa. Exchange paths compare vectors leading to the same meeting vertex; a family of one more meeting vertices than outputs then forces the stated bound. This argument uses the rendezvous geometry of Wang’s §2.

References

• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Output
• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Vertex
• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.Wins
• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.kappa
• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.n
• Truth anchor: D5/S3/Quantum/Entanglement/RendezvousVectorSystemGap.vector_system_gap
• Dependency: D5/S3/Arith/Congruence/ConditionalComparison/CommonTreeUnion
• Dependency: D5/S3/ObserverMemory/Algorithms/KBonacciAcquisition/WindowSeamCodes