Section 12 — Sandwich constructions: pasted families #
Pasted interpolation families, recurrence weights, and final operator families.
Source-style recurrence weight S_{τtail} from lem:from-H-to-G.
The parameter prefixLen is the number of type bits already converted into the
Bernoulli polynomial. This is exactly truncatedTypeSums specialized to the
averaged complete operator G = E_x ∑_g G^x_g.
Equations
- MIPStarRE.LDT.Pasting.fromHToGRecurrenceWeight params family prefixLen τtail = MIPStarRE.LDT.Pasting.truncatedTypeSums family.averagedSubMeas.total params.d prefixLen τtail
Instances For
The interpolated operator H^{x_1,\dots,x_k}_h restricted to tuples that are
globally consistent with a single polynomial.
The paper's definition (references/ldt-paper/ld-pasting.tex lines 474–495) sums
only tuples (g_1,…,g_k) in Global_τ(x) — those consistent with a single
polynomial h — and then interpolates. The |τ| ≥ d+1 eligibility filter is
applied by interpolationEligibleSandwichFamily; this definition additionally
restricts to globally consistent tuples via IsGloballyConsistent.
Consequently, pastedInterpolationFamily is supported only on tuples satisfying
both restrictions, and any fallback or default value in
interpolateCompletedSlices is irrelevant off that restricted support.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The averaged sandwiched family restricted to outcome tuples of type τ
with |τ| ≥ d+1, as in lem:over-all-outcomes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The specific pasted submeasurement constructed from the sandwich/interpolation scheme.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The distinguished fallback polynomial h₀ that receives the completion mass.
Equations
Instances For
The specific pasted measurement obtained by completing the constructed pasted submeasurement.
The paper adds all missing mass I - H_total to a single distinguished polynomial
outcome h₀ (the fallback interpolant). So the outcome operator for h₀ becomes
H_{h₀} + (I - H_total) while all other outcomes keep their original operators, and
the total is genuinely the identity I.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Degree-zero candidate pasted submeasurement obtained by averaging the slice family and viewing each slice polynomial as a polynomial in one more variable.
Paper origin: references/ldt-paper/ld-pasting.tex:12-55. This is a
Lean-only construction for the d = 0 branch of thm:ld-pasting, where the
ordinary interpolation construction is not available because d + 1 = 1
collapses the distinct-height argument. It introduces no additional
hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Evaluating the averaged appended-slice submeasurement at a next-level point is the same as evaluating the averaged slice family at the truncated point.
This is the first formal step in the degree-zero branch of thm:ld-pasting;
the later consistency rectangle compares this averaged slice construction with
the point measurement.
Placeholder family for the vertical axis-parallel line measurement B^u_f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical vertical line through u : Point params reaches appendPoint u x
at parameter x.
Pull back the vertical-line answer family along truncatePoint, then read
its line polynomial at the lifted point's final coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
In degree zero, the lifted vertical-line answer family is independent of the height coordinate once the old point coordinates are fixed.
Lean-only helper for the degree-zero branch of thm:ld-pasting; it formalizes
the fact that a vertical line answer of degree zero is constant in the line
parameter. The source context is references/ldt-paper/ld-pasting.tex:12-55.
Explicit value extracted from the i-th genuine slice outcome at the test point.
The paper's one-point sandwich comparison only sums over tuples with
g_i ≠ ⊥; the none mass is therefore removed before postprocessing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Explicit value extracted from the vertical line measurement B^u at the slice height x_i.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restrict a global polynomial-valued submeasurement to the vertical line through u.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collapse a submeasurement to its Unit-valued total operator.
Equations
Instances For
The expansion over all outcome types τ, written as the
total mass of the averaged sandwich family restricted to |τ| ≥ d+1.
Equations
- MIPStarRE.LDT.Pasting.allOutcomesExpansionFamily params _strategy family k = MIPStarRE.LDT.Pasting.pastedMeasurementTotal (MIPStarRE.LDT.Pasting.averagedEligibleSandwichSubMeas params family k)
Instances For
The one-outcome submeasurement whose unique effect is the Bernoulli-tail
operator of X.
Equations
- MIPStarRE.LDT.Pasting.bernoulliTailSubMeas k degree X hXpsd hXleOne = MIPStarRE.LDT.SubMeas.singleOutcome (MIPStarRE.LDT.Pasting.bernoulliTailOperator k degree X) ⋯ ⋯
Instances For
The Bernoulli-tail polynomial in the averaged complete operator G = E_x \sum_g G^x_g.
Equations
- MIPStarRE.LDT.Pasting.bernoulliTailFromFamily params family k = MIPStarRE.LDT.constSubMeasFamily (MIPStarRE.LDT.Pasting.bernoulliTailSubMeas k params.d family.averagedSubMeas.total ⋯ ⋯)
Instances For
Average the sandwiched completed-slice family over tuples whose completed/
incomplete pattern is exactly τtail.
This is the paper's operator
$$ \mathbb E_{x_{\ge \ell}} \sum_{g_{\ge \ell} \in \mathsf{Outcomes}_{\tau_{\ge \ell}}} \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}}, $$
written in the existing SubMeas Unit API so that its total operator is the
relevant suffix-stage matrix. Unlike the old fromHToG recurrence families,
this keeps the \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}} suffix visible instead
of collapsing immediately to the full k-step total mass.
When this is used in fromHToG, the suffix length is tailLen = k - ℓ, and
the expectation is the paper's independent uniform average over the remaining
slice points x_{≥ℓ}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stage-ℓ suffix family from the proof of lem:from-H-to-G, for a fixed
remaining tail type τ_{≥ℓ}.
This is the operator-valued quantity displayed termwise in
references/ldt-paper/ld-pasting.tex, equation
eq:i-think-this-is-what-i'm-supposed-to-prove-2 (lines 1386–1391), and in the
parallel blueprint discussion in blueprint/src/chapter/ch09_pasting.tex.
The parameter prefixLen is the Lean 0-based stage index. In the ambient
k-step recurrence where this family is used, the remaining tail length is
tailLen = k - prefixLen, so Lean stage prefixLen corresponds to the paper's
stage prefixLen + 1.
Concretely, this records $$ \mathbb E_{x_{\ge \ell}} \sum_{g_{\ge \ell} \in \mathsf{Outcomes}_{\tau_{\ge \ell}}} \widehat H^{x_{\ge \ell}}_{g_{\ge \ell}} \otimes S_{\tau_{\ge \ell}}. $$
Equations
- One or more equations did not get rendered due to their size.