Structured Preparation
Exercise SP-116
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the suffix index satisfies v(y) < M so each threshold reduces to a two-state separation across the cut
- the bound is a rank/separation certificate and asserts no circuit compiler
Question
The full target initial datum is a piecewise function: an exponential left tail for p < -1, a degree-<=2k+1 polynomial bridge for -1 <= p < 0, and an exponential right tail for p >= 0. Sample it on an integer-indexed grid and split the index as M*u(x) + v(y) across a binary cut, where v(y) < M. Prove that the resulting bivariate sample array has rank at most 8k+12, uniformly over the cut location, by exhibiting an explicit finite-width factorization. Account for every additive piece and the exact width it contributes.
Hint: mathematical route
The full exponential-polynomial-exponential sample array has cut rank at most 8k+12, assembled as 2 + 4(2k+2) + 2 from indicator, exponential, and polynomial finite-width factorizations.
- The datum splits into three indicator-selected pieces; each threshold indicator separates across the binary cut into two states.
- Left/right tails contribute width 2 each; the middle band contributes width 4*(2k+2)=8k+8.
- Summing widths gives an index set of cardinality 8k+12, bounding the sample rank uniformly over the cut.
Reference solution
Write the sampled datum as a sum of three terms selected by threshold indicators of the integer index n(x,y) = M u(x) + v(y). Let A, B be the integer cutoffs for the thresholds p < -1 and p < 0 respectively (obtained by a ceiling of an affine expression; across the cut each threshold indicator factors through width 2). Term 1 (left tail): 1[n < A] * exp(grid), width 2 * 1 = 2 (indicator times exponential). Term 2 (middle): (1[n < B] - 1[n < A]) * q(grid), where q is the source polynomial of degree <= 2k+1. The band indicator is a difference of two width-2 indicators, so by the sum/negation laws it factors through width 2 + 2 = 4; multiplied entrywise by the polynomial of width (2k+1)+1 = 2k+2 gives width 4 * (2k+2) = 8k+8. Term 3 (right tail): (1 - 1[n < B]) * exp(-grid), the complement indicator times an exponential; the complement factors through width 2 and the exponential through width 1, so width 2 * 1 = 2. Summing the three terms adds widths: 2 + (8k+8) + 2 = 8k+12. Each threshold indicator truly separates across the binary cut because 'M u(x) + v(y) < T' reduces, using v(y) < M, to a two-row condition (u(x) < T/M, or u(x) = T/M together with v(y) < T mod M) — exactly a two-state separation. The exponential separations use exp(a+b) = exp(a) exp(b) (width 1), and the polynomial separation uses the shifted-Taylor factorization (width deg+1). The combined explicit width is a finite index set of cardinality 8k+12, so the rank of the sample array is at most 8k+12, independent of the register width and of where the cut is placed. This is a separation certificate only; it does not by itself furnish a gate compiler or a finite-precision algorithm.
Assessment rubric
- Decomposes the sampled datum into left-tail, middle-band, and right-tail terms selected by threshold indicators of the cut index. (1 weight)
- Assigns widths: left tail 2 (indicator x exp), right tail 2 (complement indicator x exp). (1 weight)
- Computes the middle width 8k+8 as band-indicator width 4 (difference of two width-2 indicators) times polynomial width 2k+2. (1 weight)
- Sums the widths 2+(8k+8)+2 = 8k+12, notes threshold separation uses the v(y)<M two-state reduction, and concludes rank <= 8k+12 uniformly, flagging it is only a rank certificate. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/HermiteCutRank.lean
lines 192-248: HermiteBond k = Sum (Sum (Fin 2 x Unit) ((Sum (Fin 2)(Fin 2)) x Fin (2k+2))) (Fin 2 x Unit); hermiteBond_card = 8k+12; hermite_affine_factorization builds hleft = threshold.pointwise_mul exp, hmiddle = (hB.add hA.neg).pointwise_mul hpoly, hright = complement.pointwise_mul exp, hsum = (hleft.add hmiddle).add hright; hermite_affine_cut_rank_le : rank <= 8k+12
Source SHA-256:c0f038bd889c77163967c71df5f5987082f4b79ab7db2b7822efcdda7234aaf2· MIT (repository LICENSE)
Contract: 46eb7e594a8ff2684a4c115337a894ac884adaffe7f2d84a6da6cb9f304c1941
Item digest: 5a48d2fbfdcd90638dbcba8d09119755740f0e5606aae50d25be30c0d2c43380
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.