Exercise LA-214

Materialization has no uniform dimensions-only cost bound over unrestricted suppliers: a fixed one-by-one zero matrix can be supplied with arbitrarily many charged additions. Polynomial bounds require control of the supplier work, not merely a storage surcharge.

1. The exact materialization identity retains the nonnegative double sum S of supplier per-entry costs, plus the specified dimension-fixed storage surcharge.
2. At N=M=1, a supplier returning zero after K charged additions gives field cost K for arbitrary K. This defeats a bound uniform over all suppliers at fixed dimensions; a j-cost polynomial example alone would not.
3. A uniform polynomial bound on total supplier work S is necessary and sufficient after adding the polynomial surcharge. A uniform polynomial per-entry bound B(N,M) is a sufficient interface giving N*M*B plus surcharge.

The claimed implication is false. The issue is a uniform bound over the allowed suppliers and their inputs, not whether two suppliers can have different costs. Fix N=M=1. For each natural number K, let the sole entry supplier perform exactly K charged field additions, adding zero to a stored accumulator each time, and then return zero. This is a concrete terminating counted computation for every K, and all these suppliers return the same one-by-one zero matrix. Its field cost is K. The storage surcharge contributes no field operations, so the materialized result also has field cost K. Any proposed polynomial p(N,M) that is to bound every allowed supplier has the fixed value p(1,1). Choosing a natural K greater than that value contradicts the bound. An unbounded data parameter controlling the same loop gives the same obstruction for one supplier family at fixed dimensions. No growth in the dimensions is needed for this counterexample.

For each counter op the source identity is C_total(op)=S(op)+(N*M+N)*s(op), where S(op) is the double sum of entry-supplier costs and s(op)=2*tick(read)(op)+2*tick(write)(op). Since costs are nonnegative, a uniform polynomial-in-dimensions bound on C_total over a specified supplier/input class exists exactly when such a bound on S exists: S<=C_total, and the remaining surcharge is already polynomial. A convenient sufficient interface is a bound cost(f(i,j),op)<=B_op(N,M) for every entry and every admitted input, where B_op itself is bounded by a fixed polynomial in N,M uniformly over that class. Then C_total(op)<=N*M*B_op(N,M)+(N*M+N)*s(op). The zero-entry case has S=0 and only the stated surcharge. A bound written using an unrestricted additional parameter B is merely conditional; it is not a dimensions-only polynomial theorem until B is itself controlled in terms of the dimensions. Per-entry uniformity is a useful interface, not a claim that every particular supplier has constant cost.

The old example costing j operations per entry gives the polynomial N*M*(M-1)/2 and therefore does not refute the colleague's assertion of some polynomial upper bound. Nor does observing different costs at equal dimensions refute an upper bound. The arbitrary-K construction supplies the missing quantifier argument. All counts here belong to the declared exact-real operation model; they do not establish a finite-bit runtime bound.

1. Gives a genuinely unbounded supplier/input family at fixed positive dimensions, or another rigorous counterexample defeating every claimed uniform dimensions-only polynomial. Explains why a merely varying polynomial cost such as j per entry is insufficient. (1 weight)
2. Uses the exact additive identity and separates nonnegative supplier work S from the dimension-fixed read/write surcharge. The concrete fixed one-by-one K-addition example has materialized field cost K. (1 weight)
3. States the necessary-and-sufficient aggregate condition that S be uniformly polynomial over the specified supplier/input class, and the sufficient per-entry polynomial interface yielding N*M*B plus surcharge. Does not call an uncontrolled parameter B a dimensions-only polynomial bound or claim finite-bit certification. (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/StoredGivens.lean

  materialize75-78; materialize_cost369-374

  Source SHA-256: 87a1f69d5b138f23c96a6f77a438aa81edef27427cb2581c4defe019079d2ee4 · MIT (repository LICENSE)

Contract: 3c12b9f9957ea94a3acad1bf31966d5130946caab2c7c21f01701c4091ee1803

Item digest: c6459088608c600882dee195ea922797caf27d36a904e26ea3e2a0e0028f224a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "c676dd23f7a68be8627059eb6e12cfefe9910f62c9a635b3495675187dfae459", "predecessor_key": "qcb-core-la-214", "repair_record": "shared/repairs/la-214-uniform-supplier-bound-repair.json", "repair_record_digest": "ce7d672987cfbd1a176bae4bd3bfeb8ae9da448b0ed80c73d7a5303761d98bb0", "review_record": "reports/textbook-v1/repairs/la-214-uniform-supplier-bound-repair-review.json", "review_digest": "89a325bec0a4abff3223b7fdba84237fcb1f45f00d42b03512ed2bfde8002b83" }