Exercise LA-220

One closed core has only unit scalar boundaries and actual maximum bond1 for everyD. With at least two cores the typed internalD bonds remain, giving actual max(D,1); this structural fact is separate from minimal tensor rank and construction cost.

1. Closing both boundaries on one core gives shape1->1; with multiple cores, only outer bonds collapse while typed internalD bonds remain.
2. The actual maximum is1 for n0 regardless ofD, and max(D,1) for n>=1; evaluating the upper bound alone cannot distinguish these length cases.
3. Actual bond dimensions, minimal representation rank and the separately bounded same-run exact-real construction work are distinct quantities.

The theorem maxBond(result)<=max(D,1) is a structural upper bound for the returned dependent chain, not an equality by itself and not the minimal rank needed to represent its amplitudes. maxBond includes both outer bond dimensions. Closing the left and right boundaries makes those dimensions one, so maxBond is always at least one even when an internal typed bond has dimension zero.

To answer the question about the ACTUAL bond, inspect length as well as D. If n=0 there is exactly ONE stored core. tailChain first contracts the right length-D boundary into that core, giving shape D->1; closeLeft then contracts the left vector into the SAME core, giving shape1->1 followed by nil(1). Thus actual maxBond=1 for EVERY natural D. In particular n=0,D=2 gives actual maximum1 even though the displayed bound is2; D alone cannot characterize when the returned maximum equals one.

If n>=1 there are at least two cores. The last is contracted to terminal bond1, the first to initial bond1, but one or more internal bonds remain dimensionD in the returned type. The producer does not canonicalize/compress them in response to zero or rank-deficient entries. Its typed maximum is therefore exactly max(1,D). Hence for multi-core outputs actual maxBond=1 when D=0 orD=1, and equalsD when D>=1 (at D=1 those descriptions coincide). For D>=2 it is greater than one. At D=0 there ARE zero-dimensional internal bonds in a multi-core chain, not 'no interior bonds'; all corresponding scalar amplitudes are zero because contraction includes an empty bond sum. The positive maximum is maintained by the outer unit bonds. In the single-core D=0 case its boundary contractions are empty sums as well, giving zero amplitudes but still a typed1->1 core. No normalization was assumed anywhere.

Thus the exact structural cases are: n=0 gives1 for allD; n>=1 gives max(D,1). These follow by unfolding the actual terminal/initial/tailChain/closeLeft producer and the maxBond recursion, and agree with its denotation/refinement theorem. They do not say that the represented tensor has minimal TT rankD: a chain with all-zero entries may retain typedD bonds while representing zero.

Finally bond size by itself says nothing about construction traffic or runtime. There is a SEPARATE same-run theorem giving the exact-real stored-word total upper budget20D^2+30D+5n^2+7n+31, including boundary arithmetic/materialization, copied table references and nodes; ofTable_certified combines its value refinement with that bound. It is not derived from maxBond alone, not an exact attained cost identity, and not full arbitrary-precision finite-bit runtime. A static source reading neither executes that producer nor rechecks its kernel proofs.

1. Separates the structural upper bound from actual typed maxBond/minimal tensor rank, explains outer unit boundaries and retained internal dimensions. (1 weight)
2. Derives actual maxBond=1 for n=0 and every D; for n>=1 derives max(D,1), hence1 at D0/1 andD for D>=1. Correctly retains zero-dimensional internal bonds at D0 and notes zero amplitudes/no normalization premise. (1 weight)
3. Keeps actual bond structure separate from the source's separately proved same-run exact-real cost upper bound and finite-bit runtime; does not infer cost or minimal rank from maxBond. (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/StoredMatrixProductChain.lean

  ofTable_maxBond249-254; ofTable_certified257-265

  Source SHA-256: 7a697d064a5fddd909bba048d6adc36cb645421bd565e2357588fef1ff0449f2 · MIT (repository LICENSE)

Contract: d725a753f5c011ea653c8e37c9c5de99b25a49b605224057e1426c5cde0d6e5c

Item digest: 69e87347564a6112eb1c794b7338c946298bd98b196261c6aeb81cfb2c1c1099

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "89824ba88947fc98d212a79d3b548e480a272b0577fdce101305eb146bf3125c", "predecessor_key": "qcb-core-la-220", "repair_record": "shared/repairs/la-220-closed-chain-bond-repair.json", "repair_record_digest": "3f12d99d6c59e323aade2735a0015f43d0be7b4971c8f905cc4aaabdd28f24eb", "review_record": "reports/textbook-v1/repairs/la-220-closed-chain-bond-repair-review.json", "review_digest": "8f5c6ea9bac9fc2ce90b72ddb40f5d81385f75669b20a832f3dfe17db05aa596" }