Exercise SP-115

Finite-width witnesses compose by disjoint union, sign, Cartesian product and scalar absorption. A width-two threshold supplier requires the explicit bounded natural suffix contract; a rank-three unrestricted threshold forbids its universal extension. Constructed widths are upper bounds, and symbolic factor algebra alone carries no quantum or finite-bit resource guarantee.

1. Given real factor witnesses, concatenate inner indices to construct a sum witness of width w1+w2 and negate one factor to construct a negation witness of the same width w; cancellations can make either bound nonminimal.
2. Multiply factor entries on Cartesian-product inner indices to construct the Hadamard witness of width w1*w2, and absorb any real scalar into one factor with unchanged supplied width w, also for zero scalars/widths and empty arrays.
3. Under M>0 and natural u,v,T with every v(y)<M, Euclidean division gives the explicit two-state threshold witness; dropping the suffix condition permits the displayed rank-three counterexample. Combine this qualified supplier with additive-exponential width one and degree-at-most-d additive-polynomial width d+1 witnesses by sum/product cardinality arithmetic, without inferring minimum rank or finite-bit/quantum resources from symbolic factorization.

All widths below are widths of explicit factor witnesses, hence upper bounds on minimum width, not automatic rank equalities. Write F=AB with inner index set I of cardinality w1 and G=CD with inner index set J of cardinality w2, and use ordinary real matrix multiplication (no adjoint).

(i) F+G=[A C][B;D], with inner set I disjoint-union J, has constructed width w1+w2: summing over the two summands gives AB+CD. (ii) -F=(-A)B has the same supplied width w. (iii) Define L(x,(i,j))=A(x,i)C(x,j) and R((i,j),y)=B(i,y)D(j,y). The sum over I×J is (sum_i A(x,i)B(i,y))(sum_j C(x,j)D(j,y))=F(x,y)G(x,y), by finite distributivity and commutativity of real multiplication. The Hadamard product therefore has constructed width w1*w2, not w1+w2. (iv) cF=(cA)B has constructed width w for any c in R, including zero. All four identities also hold for zero inner widths and empty row/column sets, by the empty-sum convention.

For the threshold, put q=floor(T/M) and r=T mod M, so T=Mq+r and 0<=r<M. The natural suffix assumption 0<=v(y)<M is crucial. If u(x)<q, then M u(x)+v(y)<M(u(x)+1)<=Mq<=T. If u(x)>q, then M u(x)+v(y)>=M(q+1)>Mq+r=T. If u(x)=q, the comparison reduces to v(y)<r. Thus Θ_T(x,y)=1[u(x)<q]+1[u(x)=q]1[v(y)<r]. Take left factor L(x,:)=(1[u(x)<q],1[u(x)=q]) and right factor R(:,y)=(1,1[v(y)<r])^T. This gives width two for all admitted data; repeated or missing prefix/suffix values cause no problem. T=0 gives the zero array. If r=0, the second right component is zero. The formula does not claim that both states are always needed. M>0 avoids undefined Euclidean interpretation at zero; natural nonnegativity and the suffix bound are actual premises, not consequences of arbitrary additive variables.

The unrestricted claim is false even for natural-valued indices and positive M. Set X=Y={0,1,2}, M=1, T=3, u(x)=x and v(y)=y. Then Θ_T=[[1,1,1],[1,1,0],[1,0,0]]. Its determinant is -1 (expand along the last row), so its real rank is three. A product of a 3×2 and a 2×3 matrix has rank at most two, since all output columns lie in the span of the two left columns. This array cannot factor through width two. It violates precisely v<M at suffix values 1 and 2. The bounded-suffix condition supplies a sufficient uniform guarantee; it is not claimed necessary for every individual array to have low rank.

For the additive exponential, exp(a(x)+b(y))=exp(a(x))exp(b(y)), giving width one. For p(z)=sum_{r=0}^d c_r z^r, let i run from 0 to d and use L_i(x)=sum_{r=i}^d c_r binom(r,i) a(x)^(r-i), R_i(y)=b(y)^i. Binomial expansion gives p(a(x)+b(y))=sum_{i=0}^d L_i(x)R_i(y), of constructed width d+1. Equivalently L_i(x) is the coefficient of z^i in p(a(x)+z), exactly the shifted Taylor witness in the local source. This is valid also for d=0, the zero polynomial, and a or b equal to zero; degree is an upper bound, not a promise of d+1 independent separated terms.

For H=sum_{j=1}^N c_j product_{ell=1}^{m_j} H_{j,ell}, suppose each base factor has a supplied width W_{j,ell}. Repeated Cartesian-product construction gives each product width product_ell W_{j,ell}; scaling does not increase it; repeated disjoint-union construction gives total width sum_j product_ell W_{j,ell}. Insert W=2 only for the bounded-suffix thresholds just proved, W=1 for additive exponentials, and W=d+1 for a degree-at-most-d additive polynomial. Empty products are the all-ones array, with width one, and an empty sum is zero, with width zero. For example Θ_A E+(Θ_B-Θ_A)P has a witness of width 2+4(d+1), since a difference of the two qualified threshold arrays has width 2+2=4. Any constant weights are absorbed into left factors. This illustrates the calculus without asserting disjoint supports or cancellation when A,B are arbitrary thresholds.

A useful source-specific refinement is that the complementary bounded-suffix threshold also has width two: using the same q,r, take L_c(x,:)=(1-1[u(x)<q],-1[u(x)=q]) and the same right factor as above. Their product is 1-Θ_T. Consequently Θ_A E_+ +(Θ_B-Θ_A)P +(1-Θ_B)E_- has a witness of width 2+4(d+1)+2=4d+8 when E_± are additive exponentials. Using only the generic four laws for the complement would instead give width three for 1-Θ_B and the valid but larger total 4d+9. The smaller bound uses this additional explicit complement witness, not an unjustified cancellation of inner dimensions. This generic expression need not represent a particular piecewise function unless its cuts and pieces are separately matched.

For finite matrices any such factorization implies rank<=supplied width. Cancellation, zero scaling, low-degree or degenerate data can lower rank; for instance F+(-F)=0 can be given the sum construction's width 2w even though zero admits width zero. Thus none of the displayed construction widths is asserted minimal in general, including for empty arrays. The proof manipulates factor formulas and finite inner-index sets without needing the dense target's entries as an intermediate object. It does not say that storing all factors is dimension-free: an explicit width-w representation can store |X|w+w|Y| real entries. Nor is an efficient evaluator for arbitrary u,v,a,b or supplied factors assumed. Exact real exp, coefficients, integer comparisons and factor evaluation have not been assigned finite-bit costs. The local module is noncomputable and its FactorsThrough is an existential proposition; these witnesses are algebraic separation certificates, not a certified preprocessing algorithm, stable/normalized isometry construction, finite-precision analysis, state-preparation circuit or gate/query bound.

1. Constructs the sum witness by concatenation/disjoint union with width w1+w2 and the negation witness by changing the sign of one factor with width w. Treats these as constructed widths, not necessarily minimal ranks. (1 weight)
2. Constructs Hadamard factors on paired indices with width w1*w2 and scaling by c on one factor with unchanged supplied width w, including c=0. Justifies the double-sum factorization and does not confuse ordinary factorization with an adjoint/Gram factorization. (1 weight)
3. States and uses the positive natural M, natural T,u,v and v<M contract. Derives the quotient/remainder two-state threshold factors, plus additive-exponential width one and additive-polynomial width d+1 factors. Gives the unrestricted 3×3 threshold witness with determinant -1/rank three, explaining that it violates the omitted suffix condition. Recognizes T=0, zero remainder and degenerate bases do not require width two minimally. (1 weight)
4. Derives a finite sum-of-products witness bound by multiplying supplied widths within products and adding across sums, using only qualified threshold suppliers. Distinguishes the generic complement width-three construction from any explicit width-two refinement if used. Explains no-dense-target as a symbolic algebraic fact, not dimension-free factor storage/evaluation, finite-bit complexity, normalized state preparation or circuit/gate/query certification; handles cancellation and zero/empty boundaries honestly. (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/HermiteCutRank.lean

  lines 61-105,250-257: product_factorization width Unit; exponential_add_factorization (exp(u+v)) width Unit; FactorsThrough.add -> Sum i k; FactorsThrough.neg same i; FactorsThrough.pointwise_mul -> i x k; FactorsThrough.scale same i. lines 133-148: threshold_factorization width Fin 2

  Source SHA-256: c0f038bd889c77163967c71df5f5987082f4b79ab7db2b7822efcdda7234aaf2 · MIT (repository LICENSE)

Contract: b91f8d89b32ba3072bfa8ea635c19cb4593132a25765c41edc0a4c7f6b66af77

Item digest: 572c6321c5353ea0ac8f50e7151bd1686772620c4cb492de922633eac625d1e3

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.

{ "question_version": 2, "predecessor_key": "qcb-core-sp-115", "predecessor_item_digest": "9b1cb75533a000762b2c32c229bd35ff69abe87b9d290f07a67c8c3f56841339", "predecessor_contract_hash": "100166c122f1f17df8582b740fef87d440236690e24d51ec33f9339fb5bb906c", "current_contract_hash": "b91f8d89b32ba3072bfa8ea635c19cb4593132a25765c41edc0a4c7f6b66af77", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-115-threshold-domain-question-successor.json", "repair_record_digest": "8af0c91bc63b25aa9587cf8537e4994cc5933c93296635a5d500a3b2abd22f44", "review_record": "reports/textbook-v1/repairs/sp-115-threshold-domain-question-successor-review.json", "review_digest": "e9064d58cd9a1d70b702d0336597bb4c31c008e33d172e2003c2f6b39865a5e2", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }