Stored Cost Refinement
Exercise LA-211
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 operation tags form a finite type with exactly eight inhabitants
- Cost functions map tags to natural numbers
- Totals are operation counts in the exact-real model, not finite-bit runtimes
- Original derivation from inspected local source; no fresh Lean verification
Question
Two notions of total cost appear in the stored exact-real model. One, call it the ordinary total, is the sum of a cost function over the finite type of all operation tags. The other, call it the enumerated total, is the explicit eight-term sum field + square root + inverse-cosine + other-trig + comparison + read + write + emitted-record. Prove that these two totals are equal as functions of the cost, that the total of a sum of two costs is the sum of their totals, that the total of the zero cost is zero, and that the total of a single unit charge on one tag is one. Explain why these simple algebraic facts are exactly what licenses replacing a sum-over-tags by the fixed eight-term expression in later cost proofs.
Hint: mathematical route
Prove the sum-over-tags total equals the eight-term enumerated total, is additive, zero on the zero cost and one on a unit charge, and explain why this enables compositional cost proofs.
- Enumerating the eight tags identifies the ordinary total with the eight-term enumerated total.
- Finite summation gives additivity, the zero law and the unit-charge law.
- These laws justify computing a total term by term and switching between abstract and enumerated forms.
Reference solution
The operation tags form a finite type with exactly the eight inhabitants field, square root, inverse-cosine, other-trig, comparison, read, write, emitted-record. The ordinary total sums the cost over the universal finite set of tags. Enumerating that finite set as the eight listed inhabitants, the sum over the set equals field + sqrt + angle + trig + compare + read + write + emit, which is precisely the enumerated total; hence the two totals coincide for every cost. Additivity: the sum over tags of (a+b) applied pointwise is the sum over tags of a plus the sum over tags of b, because finite summation distributes over pointwise addition; so the total of a sum is the sum of the totals. Zero: the zero cost assigns zero to every tag, and a finite sum of zeros is zero. Unit charge: a single unit charge on one tag assigns one to that tag and zero to the others, so its total over all tags is exactly one. These facts matter because cost expressions are built compositionally by adding sub-costs and charging unit ticks; additivity lets a total be computed term by term, the zero and unit laws evaluate the leaves, and the enumeration identity lets a proof pass freely between the abstract sum-over-tags and the concrete eight-term polynomial used in the final bound. All of this concerns operation counts in the exact-real model and makes no finite-bit runtime claim.
Assessment rubric
- Prove ordinary total equals the enumerated eight-term total via finite enumeration of tags (1 weight)
- Prove additivity, the zero law, and the unit-charge law for totals (1 weight)
- Explain how these laws license term-by-term compositional cost computation (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/StoredHermiteRawCost.lean
ordinary21; ordinary_eq_total24-29; ordinary_add31-32; ordinary_zero34; ordinary_tick36
Source SHA-256:315e9f210c44c15e41742ef673ac93b191dfbbe48bb4ba84cd9abdd35f6adf62· MIT (repository LICENSE)
Contract: 2dbd921d152bf39dab3201e2309d0a81babbba0a2eac8ff994f3d1fbfaefdfe0
Item digest: 8a26d0b580fa303806b022d75965d1d39401d78114de1ccc9363c4c6c4f582c6
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.