Exercise PLAN-407

The partition estimator lambda/n is always a valid ordered spectrum, but exact equality need not ever occur for irrational r. The polynomial-qualified KL bound plus the explicit diagram count proves fixed-epsilon convergence in probability, with zero-spectrum support handled separately.

1. For n>=1,lambda/n is ordered, nonnegative and sums to1, so it is a valid candidate spectrum.
2. An irrational fixed spectrum refutes universal exact-equality consistency; only a fixed epsilon-away region has a uniform positive relative-entropy gap, with incompatible supports having zero probability.
3. Sum the polynomial-qualified outcome bound over at most(n+1)^d diagrams to obtain fixed-epsilon convergence in probability, not an exact-atom claim. This concentration subtarget overlaps319 and does not add a new core or implementation certificate.

(a) Because n>0, division preserves lambda_1>=...>=lambda_d>=0 and gives sum_i lambda_i/n=1. Thus hat r is a nonincreasing nonnegative probability vector. For example diag(hat r) is a density matrix with exactly this ordered spectrum. There is no estimator lambda/n at n=0, which is not used in this large-n statement.

(b) The claimed exact-equality consistency is false. For d=2 take rho=diag(t,1-t),t=1/sqrt(2). It is a fixed ordered full-rank state since1>t>1/2, and t is irrational. Every lambda_i/n is rational at every finite positive n, so hat r NEVER equals r. Therefore Pr(hat r!=r)=1 for every n, regardless of the sampling probabilities. This refutes the literal assertion, including the same sentence printed after source Algorithm9.1; it does not refute convergence in probability in a fixed positive tolerance.

Pointwise positivity D(p||r)>0 for p!=r cannot be promoted to a uniform delta>0 over that punctured simplex. For the same r, take k_n=floor(nt) and lambda^(n)=(k_n,n-k_n), an ordered partition for all sufficiently large n. Then lambda^(n)/n approaches r without ever equaling it, and continuity of relative entropy for this full-rank r gives D(lambda^(n)/n||r)->0. The outcomes and their exponents change with n. One cannot freeze an outcome-dependent positive exponent while shrinking the deviation radius to zero. Even the rational spectrum(1/2,1/2) cannot equal lambda/n when n is odd, so an exact-equality limit for all n is not rescued merely by rationality.

(c) Put h=d(d-1)/2. If r_i=0 and(lambda_i/n)>0 for some i, the stipulated D convention and outcome bound force w_lambda=0. Restrict attention to the closed probability face F={p:p_i=0 whenever r_i=0}. On F, the remaining r_i are strictly positive and D(p||r)=sum_{r_i>0}p_i log p_i-sum_{r_i>0}p_i log r_i is continuous, with0 log0=0. It is nonnegative and vanishes only at r. The set F_epsilon={p in F:||p-r||_1>=epsilon} is compact. If it is nonempty, its minimum delta_epsilon of D is strictly positive: a zero minimum would occur at r, excluded by epsilon>0. If it is empty, all possible positive-weight outcomes are already inside the neighborhood and the outside event has probability0.

There are at most(n+1)^d possible diagrams, because each padded row length lies in{0,...,n}; ignoring ordering and sum constraints only overcounts. Hence in the nonempty case the union bound gives Pr(||hat r-r||_1>=epsilon)=sum_{lambda:||lambda/n-r||_1>=epsilon}w_lambda <=(n+1)^[h+d]*exp(-n delta_epsilon). The exponent h+d=d(d+1)/2 includes BOTH the original per-outcome factor and the count factor; it cannot be replaced by h merely because one term has the smallest rate. Its logarithm is(h+d)log(n+1)-n delta_epsilon, which tends to minus infinity for fixed d and fixed epsilon, proving convergence in probability. If desired, natural-log Pinsker D(p||r)>=||p-r||_1^2/2 gives the explicit valid bound(n+1)^[d(d+1)/2]*exp(-n epsilon^2/2), including incompatible supports via D=+infinity. This last inequality uses the standard Pinsker theorem stated in source Eq9.41, not pointwise D positivity alone.

No full-rank hypothesis was added. At d=1 the only outcome is lambda=(n), so hat r=r=(1) surely. For rank-one r at larger d, the given bound forces zero probability outside its singleton support face, so only the matching partition can have positive weight. These special cases do not repair the universal exact-equality assertion, already refuted by the irrational full-rank example. In general the theorem proves that TOTAL probability in every fixed neighborhood tends to1; it does not show an exact matching diagram eventually exists, that its atom has probability tending to1, or that each nearby atom has a positive constant lower bound.

The valid neighborhood/relative-entropy union argument is substantially the same concentration subtarget as plan319. This successor additionally retains validation of the partition estimator and explicitly diagnoses the false exact-equality quantifier. It preserves the reserved407 identity/family/split and makes no claim of a new globally distinct core or a completed alias reconciliation. The source later Proposition9.5 is a fixed-epsilon statement; the extracted Eq9.35 omits the count factor invoked by its own text, so the explicit sum above is used rather than that shortened formula. No efficient Schur-transform circuit, finite-bit equality oracle, lower bound on exact atoms or fresh local Lean proof is inferred.

1. Proves lambda/n is an ordered probability vector for n>=1 and identifies a density matrix with that spectrum. (1 weight)
2. Explicitly refutes exact-equality consistency using the fixed irrational qubit spectrum and rational estimator grid; explains why pointwise positive KL divergence supplies no uniform punctured-simplex gap as n changes. (1 weight)
3. For fixed epsilon proves a uniform positive rate on the supported closed away-region, handles zero r_i through D=+infinity and zero outcome weights, and performs the union bound with exponent d(d-1)/2+d, not just the per-outcome exponent. (1 weight)
4. Shows the fixed-d polynomial is dominated by exp(-n delta_epsilon), states convergence in probability rather than exact equality/constant atom weights, handles d=1/rank-one boundaries, and records substantial overlap with319 without a new-core or efficient-implementation claim. (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

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: bd70d7c3406d456f52bcb1fa331f1e00117b9e38165b63dff5105473b9913f81

Item digest: f176d4884d0e3d1306f9e1f5355c0ed8b1d44d0dfc90e96d13d8e3ff3625a862

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-plan-407-spectrum-estimator-normalized-partition-validity", "predecessor_item_digest": "427b9899965fedd55c13f5e4b447607c4e9aa577d2823e36b2d746716301c9c6", "predecessor_contract_hash": "df551f43bd9ee6937018c39bad53ba61fdcec54489bfa28c58aed7307f7bfc36", "current_contract_hash": "bd70d7c3406d456f52bcb1fa331f1e00117b9e38165b63dff5105473b9913f81", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/plan-407-fixed-neighborhood-state-successor.json", "repair_record_digest": "87ffafa152bb4ce9810d460206df4bfb6f65ca0a8ed9bcee4cc966010725b33c", "review_record": "reports/textbook-v1/repairs/plan-407-fixed-neighborhood-state-successor-migration-revalidation-review.json", "review_digest": "af1857827d67396ec12130a97538070823d96d5962acdd843dad495804a7206d", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }