Exercise LA-219

The actual positive-scale compiled injection flags encode the cutoff bits: right children never inject, and each left child injects exactly at a1 bit. Hence expCalls=n+2+popcount(cutoff), with sharp attainable range n+2..n+2+max(n,1); an explicit convention-aware migration is required.

1. The actual same-run ledger is n+2 plus its true child injections; decoded compiled parent/span data force right child off and left child equal to a cutoff binary digit.
2. Choosing L=1/pi yields cutoff0 and no injection, while general legal scales realize every cutoff0..2^n; actual guards are correlated, not independent.
3. The sharp attainable E set is n+2 through n+2+max(n,1); the old3n+4 cap remains true but is unattainable on legal positive-scale inputs.

Let c be the cutoff actually returned by the compiled cache. HermiteBinaryCutoff.compute_value, tailCache_value and compile_tails identify it with Nat.ceil((-1+pi L)/h), h=pi L/2^n>0. The source proves0<=c<=M=2^n. For each t the actual input producer reads r=n-t and the span table2^r, and its parent table has p=2^(r+1) floor(c/2^(r+1)). The two children are produced once, in false/true order, with starts p and p+s, s=2^r; leftFull is exactly first+s<=c (the lower-bound0<=first is automatic). These facts are not independent flag assumptions.

Write c=2sQ+u with Q=floor(c/(2s)) and0<=u<2s. Then p=2sQ. The right child's Full condition is p+2s<=c, equivalent to2s<=u, which is impossible. The left child's condition p+s<=c is equivalent to s<=u. It is therefore true exactly when the r-th binary digit of c is1, since floor(c/s) mod2=floor(u/s) is0 or1 according as u<s oru>=s. In particular at most ONE child at each stage fires. Summing t=0,...,n visits every r=n,...,0 once. Since c<=2^n<2^(n+1), there are no higher nonzero digits, so g=sum_{r=0}^n bit_r(c)=popcount(c).

The actual stage ledger counts one exponential for each true leftFull and none for false; it does not charge exponentials for copying records, collection or ledger summation. Coefficient compilation calls exp(-1) once and the cached tails call exp once at each of n+1 levels. The actual raw producer aggregates those SAME runs. Thus E(k,n,L)=n+2+popcount(c), independent of k at this call-count level. This is a source-derived identity, not a count obtained by independently varying arbitrary booleans.

For n=0, M=1 and c is0 or1, so g is0 or1 and the attainable E set is{2,3}. For n>=1, if c<M then c uses only its n low bits and popcount(c)<=n; the endpoint c=M has exactly one1 bit and thus still g<=n. Every g=0,...,n occurs: take c=2^g-1, with c=0 when g=0. These cutoffs satisfy0<=c<M for g<=n. Consequently the full attainable set is {n+2,n+3,...,2n+2} for n>=1. Equivalently for all n>=0 it is every integer from n+2 through n+2+max(n,1), not merely a containing interval. The top cutoff c=2^n gives g=1 for EVERY n; the maximum g=n for n>=1 is attained at c=2^n-1 (at n=1 both cutoffs1 and2 have g=1). No n+1-bit-all-ones pattern is compatible with c<=2^n.

Attainability must come from positive SCALE inputs. For any desired integer c in0,...,M, write a=pi L. If c=0 choose a=1, i.e.L=1/pi>0; then(-1+a)/(a/M)=0 and Nat.ceil is0. If1<=c<=M choose a=M/(M-c+1/2)=2M/(2M-2c+1), hence L=a/pi>0. The denominator is at least1/2, so this is legal. Direct substitution gives M*(1-1/a)=c-1/2. Since c-1<c-1/2<c and c>=1, its natural ceiling is exactlyc. The actual binary cutoff theorem then ensures that the compiled producer—not just a hypothetical cache—returns thatc. This proves every cutoff in the claimed set is attainable with finite positive L, and supplies the scales for every population count above. It does not use an asymptotic L=infinity endpoint or arbitrary independent guard assignments.

For example L=1/pi gives E=n+2, immediately refuting always-two. More strongly, every right child is disabled; and for n>=1 even all n+1 left children cannot fire because the cutoff range excludes an all-ones n+1-bit number. The old cap3(n+1)+1=3n+4 remains a valid loose inequality, but is NOT attained on these legal inputs: for n=0 the sharp maximum is3<4, and for n>=1 it is2n+2<3n+4. Equality with the old loose cap would require all2(n+1) child injections, which is impossible here. The source theorem did not assert sharpness; the frozen answer promoted its loose cap to an attainable endpoint and the frozen convention incorrectly said only a cap was provable.

This sharper all-n argument is natural-language mathematics reconstructed from the actual producer and exact cut/refinement proofs, not a newly checked Lean declaration. An exact integer/Fraction screen for all cutoffs at n=0,...,10 corroborated the decoded schedule and scale formulas; finite screening is not the arbitrary-width proof. Counts do not include the bit cost of evaluating exp, exact comparisons, arbitrary-precision integer arithmetic, full normalized compilation or gate synthesis. No supplier or production theorem is changed.

1. Traces actual compiled cutoff/parents/spans to the two Full guards; proves right child never fires and left child iff cutoff bit_r=1 using quotient/remainder, so actual g=popcount(c). (1 weight)
2. Derives E=n+2+popcount(c); handles c0, c2^n and n0 correctly and proves sharp possible g set0..max(n,1), not independent-Boolean0..2(n+1). (1 weight)
3. Proves every required cutoff/count is attained by explicit legal positive L with natural ceiling checked; contrasts sharp count set with loose unattainable3n+4 cap and keeps the new NL derivation separate from existing kernel/source/finite-bit evidence. (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/StoredHermiteRawCost.lean

  stage_exponentialCalls61-68; stage_exponentialCalls_le70-72; raw_exponentialCalls181-185; raw_exponentialCalls_le187-191

  Source SHA-256: 315e9f210c44c15e41742ef673ac93b191dfbbe48bb4ba84cd9abdd35f6adf62 · MIT (repository LICENSE)

Contract: 8071360a2cb8f672ebcbb0bf3ca61da4283ffe28766652b17ede24d6cc89eb3d

Item digest: 23c1916acadef527192de759a6637e4c6182f37f3b4c7f315ff74a90e0e6d45a

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

Historical conventions (audit only)

• The exact count is guard-dependent; only an inequality cap is provable; exact-real, not finite-bit
• Original derivation from inspected local source; no fresh Lean verification

Current conventions

• The exact count depends on the correlated guards generated by the actual compiled positive-scale source. The existing Lean file supplies a valid loose cap; a sharper attainable-count analysis is additional mathematics, not forbidden by that existing evidence frontier. Exponential calls are exact-real primitive counts, not finite-bit runtime.
• Original derivation from inspected local source; no fresh Lean verification

{ "question_version": 2, "predecessor_key": "qcb-core-la-219", "predecessor_item_digest": "17529c3e96a9905183c6dae1c01a2913c0f0ccd19b569e01410ef064feb9321e", "predecessor_contract_hash": "1adc7e2fff3b379cfa59091ba192d0d9ffdd4cd49c4b0e945f9e884ce5c4ba79", "current_contract_hash": "8071360a2cb8f672ebcbb0bf3ca61da4283ffe28766652b17ede24d6cc89eb3d", "changed_contract_fields": [ "question", "conventions" ], "repair_record": "shared/repairs/la-219-correlated-guard-question-convention-successor.json", "repair_record_digest": "916e425fe58e0bd2343d7ef2ba297fa988cd2c229fa70213206e58fccd48c5ec", "review_record": "reports/textbook-v1/repairs/la-219-correlated-guard-question-convention-successor-review.json", "review_digest": "c07388524557d8754f403ce6f3223b41c97a836eadecce836488063304301e0d", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0, "original_conventions": [ "The exact count is guard-dependent; only an inequality cap is provable; exact-real, not finite-bit", "Original derivation from inspected local source; no fresh Lean verification" ], "current_conventions": [ "The exact count depends on the correlated guards generated by the actual compiled positive-scale source. The existing Lean file supplies a valid loose cap; a sharper attainable-count analysis is additional mathematics, not forbidden by that existing evidence frontier. Exponential calls are exact-real primitive counts, not finite-bit runtime.", "Original derivation from inspected local source; no fresh Lean verification" ] }