Polynomial-family interfaces for the low individual degree test #
Packaged slice-indexed polynomial-family interfaces extracted from
MIPStarRE.LDT.Test.Strategy.
Polynomial-family interfaces #
A packaged family x ↦ G^x together with its witness operators and domination targets.
The witness and dominationTarget fields store the per-slice PSD operator
Z^x and per-slice, per-polynomial operator E_u A^{u,x}_{g(u)} appearing in
the paper's boundedness hypothesis (references/ldt-paper/commutativity-G.tex,
item data-processed-boundedness). We store these operators explicitly rather
than hiding them behind ambient defaults, so each constructor must choose an
honest witness/target pair.
Callers without access to an ambient strategy can use ofSliceMeas, which takes
Z^x := ∑_g G^x_g and dominationTarget x g := G^x_g. Callers with access to a
symmetric strategy should prefer the constructor ofSymStrat,
which derives both fields from the strategy itself.
- meas : IdxProjSubMeas (Fq params) (Polynomial params) ι
- witness : Fq params → Quantum.Op ι
- dominationTarget : Fq params → Polynomial params → Quantum.Op ι
Instances For
Honest local constructor when only the slice family x ↦ G^x is available.
This uses the slice total ∑_g G^x_g as the witness operator and the concrete
outcome G^x_g as the domination target.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The averaged submeasurement G = E_x G^x: average the slice
measurements over the uniform distribution on slice heights x ∈ F_q.
Equations
- family.averagedSubMeas = MIPStarRE.LDT.averageIdxSubMeas (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) (fun (x : MIPStarRE.LDT.Fq params) => (family.meas x).toSubMeas) ⋯
Instances For
Evaluate the slice family at a point (u, x) in F_q^{m+1}.
Equations
- family.evaluatedAtNextPoint u = MIPStarRE.LDT.evaluateAt params (MIPStarRE.LDT.truncatePoint params u) (family.meas (MIPStarRE.LDT.pointHeight params u)).toSubMeas
Instances For
Averaged point operator E_u A^u_{h(u)} appearing in source-style
boundedness assumptions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Slice-wise averaged point operator E_u A^{u,x}_{g(u)} from the paper's
boundedness hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Slice-wise averaged total operator E_u \sum_a A^{u,x}_a.
For a genuine symmetric strategy this simplifies to 1, but keeping the
strategy-shaped formula explicit records where the witness comes from.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Paper-facing constructor: bundle a slice submeasurement with a symmetric strategy so that both the domination target and the witness are derived from the strategy itself.
Concretely, dominationTarget x g is the averaged slice-point evaluation
operator E_u A^{u,x}_{g(u)} from references/ldt-paper/commutativity-G.tex,
and witness x is the corresponding averaged slice-total operator
E_u \sum_a A^{u,x}_a. Since point measurements are genuine measurements, this
witness simplifies to 1, but its stored definition keeps the provenance
explicit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
- averageCompleteness : CompletenessAtLeast ψ family.averagedSubMeas.liftLeft (1 - kappa)
Instances For
- pointConsistency : ConsRel strategy.state (uniformDistribution (Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint zeta
Instances For
A family point-consistency witness forces the displayed point-consistency
error parameter ζ to be nonnegative.
- sliceSelfConsistency : SDDRel ψ (uniformDistribution (Fq params)) family.meas.toIdxSubMeas.liftLeft family.meas.toIdxSubMeas.liftRight zeta
Instances For
Paper-faithful boundedness input for slice-indexed polynomial families.
This structure encodes the boundedness item in
references/ldt-paper/commutativity-G.tex and references/ldt-paper/ld-pasting.tex.
It consists of positive witnesses Z^x, the averaged residual bound
E_x <psi| (I - G^x) tensor Z^x |psi> <= zeta, and the domination condition
Z^x >= E_u A^{u,x}_{g(u)}.
The domination condition is stated directly against the averaged point operator
from the strategy. It is not mediated through family.dominationTarget, so this
public input does not contain an additional identification bridge.
Positivity of the slice witnesses
Z^x.- sliceBoundedness : (avgOver (uniformDistribution (Fq params)) fun (x : Fq params) => ev strategy.state (leftTensor (1 - (family.meas x).total) * rightTensor (family.witness x))) ≤ zeta
Averaged residual bound
E_x <psi| (I - G^x) tensor Z^x |psi> <= zeta. - sliceDominatesAveragedPoint (x : Fq params) (g : Polynomial params) : averagedSlicePointEvaluationOperator strategy x g ≤ family.witness x
Paper domination condition
E_u A^{u,x}_{g(u)} <= Z^x.
Instances For
The boundedness residual obtained from a concrete slice family G.
Paper origin: references/ldt-paper/inductive_step.tex:461-551
(\label{thm:self-improvement-in-induction-section}), especially the boundedness
field of the slice-wise self-improvement output.
This is the induction-oriented Z^x ⊗ (I - G^x) term after replacing the
abstract slice family by the concrete G, written in the paper's
(I - G^x) ⊗ Z^x orientation.
Equations
- _hbound.storedResidual G x = MIPStarRE.LDT.ev strategy.state (MIPStarRE.LDT.leftTensor (1 - (G x).total) * MIPStarRE.LDT.rightTensor (family.witness x))
Instances For
Stored residual half of the boundedness hypothesis.
This is exactly the paper's (I-G^x) ⊗ Z^x residual bound from
references/ldt-paper/commutativity-G.tex.
Paper-faithful domination half of the boundedness hypothesis.
This is the line Z^x ≥ E_u A^{u,x}_{g(u)} from
references/ldt-paper/commutativity-G.tex.