Polynomial-family interfaces for the low individual degree test #
Packaged slice-indexed polynomial families x β¦ G^x with their witness operators and
domination targets, and the predicates (completeness, consistency with points, strong
self-consistency, boundedness) that the induction step asks of them: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/Test/StrategyPolynomialFamilies.lean in the port of
planning/c6b-plan.md (milestone M4, section "Port conventions").
A family IdxPolyFamily params π lives in the local C*-algebra π (the vendored Op ΞΉ); the
predicates that read a state take the symmetric model S : SymModel π K in place of the vendored
Ο : QuantumState (ΞΉ Γ ΞΉ), or a symmetric strategy SymStrat params.next π K, and place the
local operators on the two factors by S.L and S.R (the vendored leftTensor (ΞΉβ := ΞΉ),
rightTensor (ΞΉβ := ΞΉ)).
Not ported #
Every declaration of the vendored file has a counterpart here.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/commutativity-G.texreferences/ldt-paper/ld-pasting.texreferences/ldt-paper/inductive_step.tex
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 positive 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 (MIPStarRE.LDT.Fq params) (MIPStarRE.LDT.Polynomial params) π
The slice family
x β¦ G^xof projective submeasurements. - witness : MIPStarRE.LDT.Fq params β π
The per-slice witness operator
Z^x. - dominationTarget : MIPStarRE.LDT.Fq params β MIPStarRE.LDT.Polynomial params β π
The per-slice, per-polynomial domination target.
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 slice family of ofSliceMeas meas is meas.
The witness of ofSliceMeas meas is the slice total.
The domination target of ofSliceMeas meas is the slice outcome.
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 = MIPRE.LIDT.Co.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 = MIPRE.LIDT.Co.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
The slice-wise averaged total operator of a symmetric strategy is 1.
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
The slice family of ofSymStrat strategy meas is meas.
The witness of ofSymStrat strategy meas is the averaged slice-total operator.
The witness of ofSymStrat strategy meas is 1.
The domination target of ofSymStrat strategy meas is the averaged slice-point
evaluation operator.
Completeness of a family: its averaged submeasurement, placed on the first factor, has
mass at least 1 - kappa.
- averageCompleteness : S.CompletenessAtLeast (SubMeas.liftLeft S family.averagedSubMeas) (1 - kappa)
The averaged submeasurement
E_x G^xhas mass at least1 - kappa.
Instances For
Consistency of a family with the point measurements of a strategy on F_q^{m+1}.
- pointConsistency : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params.next)) strategy.pointMeasurement.toIdxSubMeas family.evaluatedAtNextPoint zeta
The point measurements and the evaluated family are
zeta-consistent.
Instances For
A family point-consistency witness forces the displayed point-consistency
error parameter ΞΆ to be nonnegative.
Strong self-consistency of a family: its left and right placements are zeta-close in
state-dependent distance, on average over the slices.
- sliceSelfConsistency : S.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) (IdxSubMeas.liftLeft S family.meas.toIdxSubMeas) (IdxSubMeas.liftRight S family.meas.toIdxSubMeas) zeta
The averaged squared distance of
G^x β IandI β G^xis at mostzeta.
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 β¨Ξ¨| (I - G^x) β Z^x |Ξ¨β© β€ 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 : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Fq params)) fun (x : MIPStarRE.LDT.Fq params) => strategy.state.ev (strategy.state.L (1 - (family.meas x).total) * strategy.state.R (family.witness x))) β€ zeta
Averaged residual bound
E_x β¨Ξ¨| (I - G^x) β Z^x |Ξ¨β© β€ zeta. - sliceDominatesAveragedPoint (x : MIPStarRE.LDT.Fq params) (g : MIPStarRE.LDT.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
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.