Documentation

MIPStarRE.LDT.Commutativity.Transport.FullSlice.Bridges.ClosenessCore

Core full-slice closeness-of-inner-product comparison #

Standalone closenessOfIP scalar↔tensor comparison lemma extracted from Closeness.lean per #1127. This lemma is the core tensor-form machinery that moves a trailing measurement outcome between the scalar quartic and a manifestly positive tensor register.

The tensor-form lemmas are internal to the scalar/tensor comparison recorded in docs/decisions/713-scalar-tensor-decision.md; downstream code should use the scalar public API exposed by Closeness.lean and ClosenessXEval.lean.

References #

source
theorem MIPStarRE.LDT.Commutativity.fullSliceABAB_scalar_to_BABAtensor {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (family : IdxPolyFamily params ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (hself : family.StronglySelfConsistent strategy.state zeta) :
|fullSliceABABAvg params strategy family - fullSliceBABAtensorAvg params strategy family| ≤ √zeta

Scalar-to-tensor comparison for paper eq:gcom4 (commutativity-G.tex lines 332-337).

One closenessOfIP application moves the trailing G^x_g in the scalar quartic G^y_h G^x_g G^y_h G^x_g ⊗ I to the right register, producing the manifestly PSD tensor form G^y_h G^x_g G^y_h ⊗ G^x_g. The scalar side is stated as fullSliceABABAvg; the proof first uses the (x,g) ↔ (y,h) swap symmetry above to identify the averaged BABA scalar with the averaged ABAB scalar.