Section 12 pasting: over all outcomes — nonglobal-mass decomposition #
Nonglobal-mass definitions, the vertical-line insertion, and the line-consistency
decomposition that splits the nonglobal eligible mass into the bad-line event and
the line-consistent residual: the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/Pasting/ComparisonLemmas/OverAllOutcomes/NonglobalDecomposition.lean
in the port of planning/c6b-plan.md (milestone M11, section "Port conventions").
A strategy is a SymStrat params.next 𝔓 K and a slice family an IdxPolyFamily params 𝔓; the
masses are strategy.state.subMeasMass of left-placed submeasurements and the inserted masses
strategy.state.ev (strategy.state.opTensor T B_f). The vendored proofs unfold leftTensor,
opTensor and ev to matrices; here the insertion of the vertical-line measurement is
S.L T = S.opTensor T 1 (map_one, mul_one) followed by S.opTensor_sum_right_univ and
S.ev_sum, and the pointwise splits are S.ev_mono and S.opTensor_mono_left.
subMeasMass_restrict_add_not, a lemma on a placement, takes the model S as an explicit
first argument.
The vendored file has no classical declaration of its own; the error hBConsistencyError and
the scalar averaging lemmas are named through explicit open lists.
Not ported #
Nothing: every vendored declaration has a counterpart of the same name.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/ld-pasting.texblueprint/src/chapter/ch09_pasting.tex
Distinct-tuple mass of interpolation-eligible but globally inconsistent outcomes.
This is the scalar quantity bounded in ld-pasting.tex lines 1174--1275 when the
proof removes the Global_τ(x) restriction. It is the exact local residual
between the all-outcomes expansion over distinct tuples and the pasted/global
part.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Scalar mass splits into globally consistent and nonglobal parts.
Distinct eligible mass splits into pasted/global mass plus nonglobal mass.
The distinct-tuple line-mismatch mass that appears after inserting the
vertical-line measurement in ld-pasting.tex lines 1178--1202.
This is the part paid for by the already-available one-point line comparison
statements. The remaining md/q Schwartz--Zippel term is kept separate below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The one-point line comparison hypotheses bound the inserted line-mismatch
mass by the displayed hBConsistency error.
Paper route: this is the aggregation in ld-pasting.tex lines 1186--1202,
using prop:ld-dnoteq plus lem:ld-sandwich-line-one-point.
The vertical-line measurement is a genuine measurement, so its total is 1.
This is the formal counterpart of the line because B is a measurement at
ld-pasting.tex lines 1178--1180.
Local version of eq:B-appears-out-of-thin-air for one distinct tuple xs and
one vertical-line question u.
It inserts the vertical-line measurement into the nonglobal eligible mass.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The residual line-consistent nonglobal mass after the line-mismatch event has been split off.
This is the formal version of the consistent indicator term in
ld-pasting.tex lines 1204--1232, before applying the interpolant witness and
Schwartz--Zippel. It keeps the inserted vertical-line measurement explicit: for
each line answer f, we retain exactly the nonglobal eligible outcomes for which
no supported slice disagrees with f along the sampled vertical line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Distinct-tuple average of the line-consistent nonglobal mass.
Paper anchor: this is the explicit line-answer term just before the
Consistent_τ(g,y,u) indicator in ld-pasting.tex lines 1204--1232. The next
lemmas sum out the inserted measurement and reduce it to that indicator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Local consistency-indicator mass after summing out the inserted vertical-line measurement.
For fixed u and xs, it retains nonglobal eligible tuples for which there
exists some degree-d vertical-line answer matching every supported slice at u.
This is the Lean counterpart of the indicator
Consistent_τ(g,y,u) introduced at ld-pasting.tex lines 1204--1219.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Distinct-tuple average of the consistency-indicator nonglobal mass.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Inserting the vertical-line measurement leaves the local nonglobal mass unchanged.
Pointwise split: after inserting the vertical-line measurement, every nonglobal outcome either contributes to the already-paid bad-line event or to the line-consistent residual.
The explicit line-answer version of the line-consistent residual is bounded by its consistency-indicator version, after summing out the vertical-line measurement.
Averaged line-consistent residual after the explicit line answer is summed out.
Strict reduction of the old local residual: the nonglobal mass is bounded by the already-isolated line-mismatch mass plus the narrower line-consistent nonglobal residual.
This proves the insertion and finite-sum split from ld-pasting.tex lines
1174--1228. The following indicator lemma then sums out the inserted measurement;
together they reduce the residual to the Schwartz--Zippel estimate at lines
1235--1275.