Stored Cost Refinement
Exercise LA-217
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
- Persistent append copies only the left spine and shares the right list
- Append is charged the left length on the read and write counters
- Cost is asymmetric in the two operands; exact-real operation count, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
When a stored sweep concatenates its chronological step logs, it uses a persistent list append that copies the spine of the left list while sharing the right list unchanged; the append is charged exactly the length of the left list in reads and the same in writes, with the right list contributing nothing. A colleague asserts two things: first that appending two logs is a constant-cost pointer operation, and second that the cost depends on the total number of records in both logs. Show that both assertions are wrong by exhibiting append costs for concrete left/right lengths, and state the exact rule the cost actually follows.
Hint: mathematical route
Counterexample: persistent log append costs the left length in reads and writes and is independent of the right length, so it is neither constant nor total-length dependent.
- Append charges the left list length in both reads and writes.
- The shared right list contributes zero, so equal total lengths can have very different costs.
- The exact rule depends only on the left length, as used in the sweep cost bound.
Reference solution
Both assertions are wrong. Against the constant-cost claim: appending a left list of length p costs p reads and p writes, which grows without bound as p grows, so it is not constant; for example a left log of 100 records costs 100 reads and 100 writes regardless of pointer sharing. Against the total-length claim: the right list is shared, not copied, so it contributes zero to the cost; appending a left list of length 2 to a right list of length 1000 costs only 2 reads and 2 writes, not 1002. Concretely, left length 2 and right length 1000 cost (2,2); left length 1000 and right length 2 cost (1000,1000); same total length, vastly different cost, which also disproves any dependence on the sum. The exact rule is: the persistent append cost equals the left list's length on both the read and write counters and is independent of the right list's length, because only the left spine must be rebuilt to point into the shared right tail. This is an operation count in the exact-real model with no finite-bit content; the asymmetry is the whole point of charging prefix copying rather than a fictitious constant or total-length cost.
Assessment rubric
- Refute constant cost by showing cost grows with left length (1 weight)
- Refute total-length dependence by showing the shared right list contributes zero, with a concrete asymmetric pair (1 weight)
- State the exact rule: cost equals left length in reads and writes, independent of right length (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/StoredRectangularGivens.lean
append21-22; sweep_cost_le67-89
Source SHA-256:f8638a6d287b3b984fa530b13eeb18e3992904543236bd0756eda41fa6490d98· MIT (repository LICENSE)
Contract: e55f99b164a91b39d4e68ec8efe0a5163ec0780d2b8fd9b7778e9b1c272e26e7
Item digest: cf1248c62cc4a15751ecfbedf58495f047548317dc6baee60b7e784b4f6e4d99
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.