Reverse insertion endpoints for the evaluated-slice paper chain

This module re-exports the two reverse eq:add-an-a bounds used after the paper line-87 phase-five removal and packages them into the combined phase-67 bridge consumed by ProcessedG.lean.

theorem MIPStarRE.LDT.Commutativity.evaluatedSlice_phaseSixSeven_reverse_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) (zeta : Error) (hnorm : strategy.state.IsNormalized) (family : IdxPolyFamily params ι) (hcombined_fst : SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.1) (fun (q : EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.1) (4 * zeta)) (hcombined_snd : SDDRel strategy.state (uniformDistribution (EvaluatedSliceQuestion params)) (fun (q : EvaluatedSliceQuestion params) => evaluatedPointFamilyLeft params family q.2) (fun (q : EvaluatedSliceQuestion params) => Preliminaries.totalSandwichFamily (evaluatedPointFamily params family) (evaluatedSlicePointMeas params strategy) q.2) (4 * zeta)) : have 𝒟 := uniformDistribution (EvaluatedSliceQuestion params); have phase5PaperRemoved := evaluatedSlicePhaseFivePaperRemoved params strategy family; have phase7GonnaCite := evaluatedSlicePhaseSevenGonnaCite params strategy family; |avgOver 𝒟 phase5PaperRemoved - avgOver 𝒟 phase7GonnaCite| ≤ 4 * √zeta

Paper lines 99--104: the combined phase-67 reverse-insertion bridge.

The scalar-chain assembly only needs the endpoint comparison from the paper line-87/eq:gcom10 term to eq:gonna-cite-this-in-just-a-bit. This lemma packages the two proved eq:add-an-a reverse insertions (2√ζ each) through one triangle inequality, so downstream code no longer has to carry the intermediate phase-six endpoint.