Finite Synthesis Gram Distance

Abstract

Finite synthesis into a Hilbert space gives a singular Gram formula for projection and distance.

Universally, k is an RCLike field, E is a finite-dimensional inner-product space, and H is a complete inner-product space over k. Every V below is continuous and k-linear. Set S = range V, G = V* V and b = V* x. P denotes the independently defined orthogonal projection onto S, infDist is the metric infimum over S, and MP is the constructed Moore-Penrose inverse. No injectivity or invertibility is assumed.

Theorem 1.1 (Operator projection identity).

$$\forall V:E{\to }_{k}H,P_S=V\mathrm{MP}(G)V^{\ast }$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_projection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The adjoint target lies in the Gram range. The first Penrose law then yields the normal equation, and the residual is orthogonal to the entire synthesis range. Projection uniqueness gives the displayed equality of operators on H.

Theorem 1.2 (Squared infimum distance).

$$\forall V:E{\to }_{k}H,\forall x\in H,\mathrm{infDist}(x,S{)}^2=\Vert x{\Vert }^2-\Re (⟨b,\mathrm{MP}(G)b⟩)$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_distance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Projection minimality identifies infDist with the residual norm; the squared-norm expansion gives the Gram quadratic expression.

Theorem 1.3 (Reality of the quadratic expression).

$$\forall V:E{\to }_{k}H,\forall x\in H,⟨b,\mathrm{MP}(G)b⟩=\Vert P_{S}x{\Vert }^2$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_quadratic (✓ std3). ∎

Source. Repository-derived.

Commentary.

The nonnegative real squared norm on the right is coerced into k. Thus over the complex field this proves reality as well as the value.

Theorem 1.4 (Identification with the ordinary inverse).

$$\forall A:E{\equiv }_{k}E,\mathrm{MP}(A)=A^{-1}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.moore_penrose_eq_inverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

A is any linear equivalence on E. Its ordinary inverse satisfies all four laws, so the imported uniqueness theorem applies.

Theorem 1.5 (Invertible Gram specialization).

$$\forall V:E{\to }_{k}H,\forall x\in H,\forall G:E{\equiv }_{k}E,G=V^{\ast }V\Rightarrow \mathrm{infDist}(x,S{)}^2=\Vert x{\Vert }^2-\Re (⟨b,G^{-1}b⟩)$$

Proof. Machine-checked in Lean as D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_distance_inverse (✓ std3). ∎

Source. Repository-derived.

Commentary.

Only this specialization assumes that the Gram operator is a linear equivalence. The singular case remains covered by the preceding identities.

Application: a fixed coherent affine constraint.

Let ι be any finite nonempty index set, let i₀ be one of its elements, and let H be a finite-dimensional complex Hilbert space. Thus the number of amplitudes is at least one. For any actual family x : ι → H, retain its fixed cross-input complex phases. Give the coefficient space C^ι its usual Euclidean inner product, conjugate-linear in the first slot. The following application uses the actual synthesis and its Gram operator:

$Xc={\sum }_{j\in \iota }{c}_j{x}_j,G=X^{\ast }X,b=1$

$D={\mathrm{span}}_{\mathbb{C}}\{x_j-x_{i_0}:j\in \iota \},q=P_{D^{\perp }}{x}_{i_0},t_{\ast }=\Vert q{\Vert }^2$

Every coefficient vector c has Gram energy equal to the real squared norm of its synthesis. Since b has every coordinate equal to one, the constraint is exactly sum c_j = 1, without conjugating the coefficients or changing the input phases.

$\forall c\in {\mathbb{C}}^{\iota },⟨c,Gc⟩=\Vert Xc{\Vert }^2,⟨b,c⟩={\sum }_{j\in \iota }{c}_j$

$\forall z\in H,(\exists c\in {\mathbb{C}}^{\iota },{\sum }_{j\in \iota }{c}_j=1\wedge Xc=z)\iff z-x_{i_0}\in D$

For the forward affine-image inclusion, subtract x_i₀ and distribute the coefficient sum. For the reverse inclusion, write z − x_i₀ as a linear combination of x_j − x_i₀, then add 1 minus the sum of those coefficients to the i₀ coordinate. This gives actual feasible coefficients. Projection gives q − x_i₀ in D and q orthogonal to D. Consequently q is feasible and the minimum is attained:

${\min }_{c\in {\mathbb{C}}^{\iota },{\sum }_{j\in \iota }{c}_j=1}⟨c,Gc⟩=t_{\ast }=\Vert q{\Vert }^2$

$\exists c_{\ast }\in {\mathbb{C}}^{\iota },{\sum }_{j\in \iota }(c_{\ast }{)}_j=1\wedge X{c}_{\ast }=q\wedge ⟨c_{\ast },G{c}_{\ast }⟩=t_{\ast }$

$\forall c\in {\mathbb{C}}^{\iota },{\sum }_{j\in \iota }{c}_j=1\Rightarrow \Vert Xc{\Vert }^2=\Vert q{\Vert }^2+\Vert Xc-q{\Vert }^2\ge t_{\ast }$

Range case, including singular Gram operators.

Take G⁺ to be the constructed Moore-Penrose inverse, not an assumed optimization oracle. Suppose b lies in range G and put p = G⁺b. The first Penrose law gives Gp = b. Hence a = ⟨b,p⟩ is the real number ‖Xp‖². It is strictly positive: Xp = 0 would imply Gp = 0 and then b = 0, impossible for a nonempty coefficient set.

$b\in \mathrm{range}G\Rightarrow p=G^{+}b,Gp=b,a=⟨b,p⟩=\Vert Xp{\Vert }^2>0$

$c_{\ast }=a^{-1}p,{\sum }_{j\in \iota }(c_{\ast }{)}_j=1,⟨c_{\ast },G{c}_{\ast }⟩=t_{\ast }=a^{-1}$

For any feasible c, the normal equation makes Xc_* orthogonal to X(c − c_*). The squared-norm decomposition proves minimality, so this explicit normalized Moore-Penrose vector attains the same minimum as q. No invertibility of G is used.

Nonrange case and an actual kernel minimizer.

If b does not lie in range G, the identities range G = (ker G)⊥ and ker G = ker X supply a kernel vector k whose inner product with b is nonzero. Normalize that vector by this inner product:

$\neg (b\in \mathrm{range}G)\Rightarrow \exists k\in \ker G,⟨b,k⟩\ne 0$

$c_{\ast }=\frac{1}{⟨b,k⟩}k,{\sum }_{j\in \iota }(c_{\ast }{)}_j=1,G{c}_{\ast }=0,X{c}_{\ast }=0,⟨c_{\ast },G{c}_{\ast }⟩=t_{\ast }=0$

This produces an actual feasible minimizer even at the singular boundary. In the range case the value is (b*G⁺b)⁻¹ with a strictly positive real denominator; in the nonrange case it is zero.

Interpretation and realization boundary.

For a common-output task, the same linear contraction must act on every input, and the common output includes all records in that branch. Its coherent budget compares t |sum c_j|² with ‖Xc‖² for every complex c; restricting to sum c_j = 1 gives the optimizer above. The algebra does not replace a fixed-phase amplitude family by its rays or discard input-dependent records. It supplies an abstract optimum and coefficients, not a native finite gate word, coherent control, or availability of the exact projection as a physical branch.

The application uses the finite Moore-Penrose construction and Penrose laws from FiniteMoorePenroseInverse, the Gram and projection identities above, and the standard range/kernel, span and orthogonal-decomposition identities in Mathlib. Its source application is the finite common-branch Gram optimum in AURIC_SHARED_CONTENT_COMPATIBILITY_QUANTUM_ADDRESSING_AND_MAXIMAL_COMMON_BRANCH_V81. The constrained formula is an application of these results.

References

• Truth anchor: D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_distance
• Truth anchor: D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_distance_inverse
• Truth anchor: D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_projection
• Truth anchor: D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.finite_synthesis_gram_quadratic
• Truth anchor: D5/S3/Observer/Hilbert/FiniteSynthesisGramDistance.moore_penrose_eq_inverse
• Dependency: D5/S3/Observer/Hilbert/FiniteMoorePenroseInverse