Stored Cost Refinement
Exercise LA-215
nl bridge from inspected source. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- The angle routine returns zero early when the computed norm is zero
- The angle budget bounds every counter for all inputs
- The budget is a branch-independent upper bound, not an exact per-input count; exact-real, not finite-bit
- Original derivation from inspected local source; no fresh Lean verification
Question
The elimination-angle routine in the exact-real model computes a norm from two inputs x and y: it squares both, adds them, takes a square root, and tests whether that root is zero. If the root is zero it returns the angle zero immediately; otherwise it divides, takes an inverse cosine, tests the sign of y, conditionally negates, doubles, and negates again. A branch-independent angle budget of seven field operations, one square root, one inverse-cosine and two comparisons is proved to be an upper bound on the angle cost for all inputs. A colleague concludes that every call to the angle routine performs exactly one inverse-cosine call. Refute this with a specific input, and explain the precise logical relationship between the proved budget and the actual per-input cost.
Hint: mathematical route
The angle budget is a componentwise upper bound. Zero inputs use no inverse cosine; nonzero inputs use one, but the full field budget is attained only when the negative-y sign branch executes its extra subtraction.
- At x=y=0 the early return has (field,sqrt,angle,compare)=(3,1,0,1), so the universal one-inverse-cosine assertion is false.
- Nonzero-root inputs have (6,1,1,2) for nonnegative y and (7,1,1,2) for negative y; both are bounded by the declared (7,1,1,2) budget, which need not equal the actual tuple.
- Componentwise bounds can be summed across actual calls, without upgrading the budget to an exact per-call arithmetic count or a finite-bit theorem.
Reference solution
Take x=y=0. The routine executes two field multiplications and one field addition, one square-root call and one zero comparison. The root is zero, so it returns the literal angle zero immediately. It executes no division, inverse cosine or sign comparison. Thus the inverse-cosine count is zero, disproving the claim that every input makes exactly one such call.
To distinguish an upper bound from an exact cost, order the relevant counters as (field,sqrt,angle,compare). The zero-root branch has exact tuple (3,1,0,1). On a nonzero-root branch, division, inverse cosine, the sign comparison, doubling and final negation are performed. If y is nonnegative the intermediate sign is passed through without a charged subtraction, so the tuple is (6,1,1,2). If y is negative the extra subtraction 0-a is performed and the tuple is (7,1,1,2). In angle itself all trig/read/write/emit counters are zero. Concrete inputs (1,0) and (0,-1) realize the two respective nonzero cases. A charged subtraction still counts when its numerical result happens to be zero; this is a counted execution trace, not an algebraically optimized expression.
The branch-independent budget is (7,1,1,2), componentwise, with the other counters zero. Every actual tuple is bounded by it. The full budget is attained on the negative-y nonzero branch, not on every nonzero input: the nonnegative-y nonzero branch uses only six field operations. One inverse cosine is exact for either nonzero branch, whereas the zero branch uses none. Summing componentwise inequalities gives a valid budget for many calls; it does not turn those inequalities into per-input equalities. Source counters that separately prove an exact emit count do not make this angle budget exact. These are exact-real operation counts, not a finite-bit or numerical-stability result.
Assessment rubric
- Exhibits x=y=0, traces the early return and obtains zero inverse-cosine calls, with no division or sign test. (1 weight)
- Explains componentwise upper-bound semantics and distinguishes full-budget equality from inverse-cosine equality. Does not claim the full budget is attained on every nonzero input; the negative-y branch uses seven field operations and the nonnegative-y branch six. (1 weight)
- Justifies summing the valid cost inequalities without inferring exact per-call counts. Keeps charged exact-real operation counts distinct from simplification, finite-bit runtime and unrelated exact emit theorems. (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/StoredGivens.lean
angle88-100; angleBudget253-255; angle_cost_le257-261
Source SHA-256:87a1f69d5b138f23c96a6f77a438aa81edef27427cb2581c4defe019079d2ee4· MIT (repository LICENSE)
Contract: 7f3d8c353f2e2a2346554be969bca19d41dae7ce9bb3ba7a78e64ce9af1375dc
Item digest: 8853829f9e72f7f223d2931d8d7c112de8c4eaacfc1853f545a2401b7d432dbb
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "5a8b2818c7e3028baaecd34a3473244b7bc65f2379c41f21d8fbabf8c03de06a", "predecessor_key": "qcb-core-la-215", "repair_record": "shared/repairs/la-215-branch-cost-repair.json", "repair_record_digest": "414a8f8ffaaf04545b35a1af1e917621f9e85b4522fc218304f1ed4bc0da949d", "review_record": "reports/textbook-v1/repairs/la-215-branch-cost-repair-review.json", "review_digest": "04938fb0237333e396dd2bee3c87c52d17ae2c31f4242a70d7faffec39200d75" }