Where the sources disagree or the structure was guessed, ranked. 71 items · 4 warn · 67 info. In v1 these are paper-internal; Lean-vs-paper rows arrive in Phase 2.
| Severity | Kind | Node | Note | Source |
|---|---|---|---|---|
| warn | unresolved_ref | Proof rests essentially on external results: Williams's witness-circuit argument [Wil13], the JMV13 local reduction, and Zak's nondeterministic time hierarchy. | main_full_version.tex:183 | |
| warn | unresolved_ref | Per-branch exponent uses the unlabeled cost estimate eq:three-costs from Section 3.5. | main_full_version.tex:1640 | |
| warn | unresolved_ref | Counting each leaf relies on the unlabeled sparse-formula argument of Section 6.3 (eq:sparse-formula-cost) rather than a statement. | main_full_version.tex:3570 | |
| warn | unresolved_ref | The proof environment only assembles the algorithm; the key recursion identity (eq:tensor-recursion-identity), mode expansion and mode-tuple count (eq:tensor-partition-count), and precision bound (eq:tensor-precision-bound) are argued in unlabeled text of D.4.4-D.4.6. | quantitative-reduction.tex:26 | |
| info | structure_uncertain | Skeleton records only the fixed-density proof (quantitative-reduction.tex:67-98); a second proof of the arbitrary-density bound is at quantitative-reduction.tex:317-361, and the combined single algorithm is described at 363-369. | main_full_version.tex:73 | |
| info | structure_uncertain | claim "Sparsify with sigma about 1/sqrt(log n)" (quantitative-reduction.tex:319-328) lies outside the recorded proof; a second proof or an appendix | main_full_version.tex:73 | |
| info | structure_uncertain | claim "Leaf counts via parity rows and contraction queries" (quantitative-reduction.tex:330-345) lies outside the recorded proof; a second proof or an appendix | main_full_version.tex:73 | |
| info | structure_uncertain | claim "Arbitrary-density time and space accounting" (quantitative-reduction.tex:347-360) lies outside the recorded proof; a second proof or an appendix | main_full_version.tex:73 | |
| info | inferred_dep | critique: The enumeration bound 2Qr C_q(2D+1)^{2τn}2^{2n/r} in Prop 3.4 rests on eq:boolean-enumeration. Line 1980 obtains that bound via "Lemma therefore computes the restricted sum". The proof at line 2033 cites eq:boolean-enumeration directly, but the DAG has no edge to the lemma. | main_full_version.tex:2013 | |
| info | inferred_dep | critique: The proof of Prop 3.4 (main_full_version.tex:2036-2037) says "The preceding Taylor identity and interpolation prove correctness". That identity, eq:full-taylor-sum, comes from "Apply Lemma to [z^j]G_x" at line 1964. The edge is missing, which also leaves the lemma an orphan. | main_full_version.tex:2013 | |
| info | inferred_dep | critique: The statement of Prop 3.4 (line 2018) requires that the data "satisfy Definition ", and the proof uses that design throughout. The DAG has no edge. | main_full_version.tex:2013 | |
| info | inferred_dep | the statement's design satisfying Definition is used; the proof relies on the layout's rows and denominators (the \ref in the statement text) | main_full_version.tex:3044 | |
| info | inferred_dep | "the rows have common denominator d_den=(R-1)!Q!" is the content of the row-coefficient lemma | main_full_version.tex:3044 | |
| info | inferred_dep | critique: Prop 5.3 takes d_H from eq:origin-residue (line 3049). That degree bound and the residue identity come from Lemma total-order: "Lemma bounds the input degree ... By the same lemma, summing their values gives" (lines 3024-3035). | main_full_version.tex:3044 | |
| info | inferred_dep | critique: Lemma 6.2 opens "With and from Lemma " (line 3447). Its proof uses the weight bound |supp v(x)| ≥ m/P from that lemma (line 3470). The DAG has no edge. | main_full_version.tex:3446 | |
| info | inferred_dep | Appendix proves the lemma, including the disjointness (the branching rule partitions satisfying assignments of the parent) | main_full_version.tex:3543 | |
| info | inferred_dep | the appendix proving this lemma (app:sparsify) contains the marked-degree counting bound used in the occurrence bound B | main_full_version.tex:3543 | |
| info | inferred_dep | the appendix proving this lemma (app:sparsify) contains the insertion bound used for depth and node count | main_full_version.tex:3543 | |
| info | structure_uncertain | No proof environment; Appendix A (main_full_version.tex:3636-3884) proves it using Lemmas A.1-A.3 plus unlabeled tree-size and leaf-bound arguments. | main_full_version.tex:3543 | |
| info | inferred_dep | critique: Prop 6.4 counts each leaf "by the sparse-formula algorithm of Section 6.3" (line 3600). That algorithm is built on Lemma greedy-hashes ("The final count is #F by the greedy lemma", line 3526). The proof also says "initial checks, and additional rows are computed by the deterministic procedures above". | main_full_version.tex:3570 | |
| info | structure_uncertain | Used in prose (child edge bound at quantitative-contraction.tex:525) outside any proof environment; the skeleton records no ref edge to it. | quantitative-contraction.tex:114 | |
| info | inferred_dep | outline: "Clause decoder as linear-size circuit" rests on claim-cor-quantitative-circuits-1 | quantitative-circuits.tex:18 | |
| info | inferred_dep | outline: "Witness language W lies in E^NP" rests on claim-cor-quantitative-circuits-1 | quantitative-circuits.tex:27 | |
| info | inferred_dep | outline: "Small witness circuits give nondeterministic algorithm for H" rests on claim-cor-quantitative-circuits-2 | quantitative-circuits.tex:46 | |
| info | inferred_dep | outline: "Small witness circuits give nondeterministic algorithm for H" rests on claim-cor-quantitative-circuits-3 | quantitative-circuits.tex:46 | |
| info | inferred_dep | outline: "Test-circuit runtime contradicts time hierarchy" rests on claim-cor-quantitative-circuits-4 | quantitative-circuits.tex:58 | |
| info | inferred_dep | outline: "Test-circuit runtime contradicts time hierarchy" rests on claim-cor-quantitative-circuits-5 | quantitative-circuits.tex:58 | |
| info | inferred_dep | outline: "Per-branch design from parameter lemma" rests on claim-thm-overview-sparse-polynomials-1 | main_full_version.tex:3129 | |
| info | inferred_dep | outline: "Per-branch running time and total exponent" rests on claim-thm-overview-sparse-polynomials-2 | main_full_version.tex:3170 | |
| info | inferred_dep | outline: "Per-branch running time and total exponent" rests on prop:count | main_full_version.tex:3170 | |
| info | inferred_dep | outline: "Per-branch running time and total exponent" rests on prop:general-count | main_full_version.tex:3170 | |
| info | inferred_dep | outline: "Polynomial space by sequential branches" rests on claim-thm-overview-sparse-polynomials-1 | main_full_version.tex:3199 | |
| info | inferred_dep | outline: "Tuple-by-tuple evaluation algorithm" rests on claim-lem-measurement-separation-1 | main_full_version.tex:1850 | |
| info | inferred_dep | outline: "Enumeration count and space bound" rests on claim-lem-measurement-separation-2 | main_full_version.tex:1868 | |
| info | inferred_dep | outline: "Conditional expectations yield balanced labels" rests on claim-lem-incidence-labels-1 | main_full_version.tex:2496 | |
| info | inferred_dep | outline: "Exact polynomial-time conditional expectation computation" rests on claim-lem-incidence-labels-2 | main_full_version.tex:2512 | |
| info | inferred_dep | outline: "Interpolation interval and binomial tail bound" rests on claim-lem-incidence-parameters-1 | main_full_version.tex:2796 | |
| info | inferred_dep | outline: "Three cost terms are balanced" rests on claim-lem-incidence-parameters-1 | main_full_version.tex:2819 | |
| info | inferred_dep | outline: "Exact computation and checking of parameters" rests on claim-lem-incidence-parameters-1 | main_full_version.tex:2828 | |
| info | inferred_dep | outline: "Exact computation and checking of parameters" rests on claim-lem-incidence-parameters-2 | main_full_version.tex:2828 | |
| info | inferred_dep | outline: "Existence and search of epsilon-biased shifts" rests on claim-lem-sparse-checks-1 | main_full_version.tex:3301 | |
| info | inferred_dep | outline: "Expander mixing bound from small bias" rests on claim-lem-sparse-checks-2 | main_full_version.tex:3336 | |
| info | inferred_dep | outline: "Tanner code nonzero words have large weight" rests on claim-lem-sparse-checks-3 | main_full_version.tex:3392 | |
| info | inferred_dep | outline: "Tanner code nonzero words have large weight" rests on claim-lem-sparse-checks-4 | main_full_version.tex:3392 | |
| info | inferred_dep | outline: "Shortened code: row count and sparsity" rests on claim-lem-sparse-checks-5 | main_full_version.tex:3418 | |
| info | inferred_dep | outline: "Total number of recursive calls" rests on lem:tensor-packets | quantitative-contraction.tex:571 | |
| info | inferred_dep | outline: "Total number of recursive calls" rests on lem:tapered-hermite | quantitative-contraction.tex:571 | |
| info | inferred_dep | outline: "Leaf cost and overall time bound" rests on claim-thm-tensor-contraction-2 | quantitative-contraction.tex:589 | |
| info | inferred_dep | outline: "Multilinear incidence polynomial with linear degree" rests on claim-lem-tensor-sparse-query-1 | quantitative-reduction.tex:144 | |
| info | inferred_dep | outline: "Indexing monomials with O(n log log n) wires" rests on claim-lem-tensor-sparse-query-2 | quantitative-reduction.tex:192 | |
| info | inferred_dep | outline: "Network contractions sum to the branch polynomial" rests on claim-lem-tensor-sparse-query-2 | quantitative-reduction.tex:241 | |
| info | inferred_dep | outline: "Network contractions sum to the branch polynomial" rests on claim-lem-tensor-sparse-query-3 | quantitative-reduction.tex:241 | |
| info | inferred_dep | outline: "Test-group entries by subset inversion" rests on claim-lem-tensor-sparse-query-4 | quantitative-reduction.tex:271 | |
| info | inferred_dep | outline: "Apply contraction theorem and total cost" rests on claim-lem-tensor-sparse-query-3 | quantitative-reduction.tex:294 | |
| info | inferred_dep | outline: "Apply contraction theorem and total cost" rests on claim-lem-tensor-sparse-query-5 | quantitative-reduction.tex:294 | |
| info | inferred_dep | outline: "Quotients by E_t lose no precision" rests on claim-lem-tapered-hermite-1 | quantitative-contraction.tex:295 | |
| info | inferred_dep | outline: "Two-adic loss of E_t(0) at most 6Dh" rests on claim-lem-tapered-hermite-1 | quantitative-contraction.tex:301 | |
| info | inferred_dep | outline: "Stated precisions recover F(0) mod 2^p" rests on claim-lem-tapered-hermite-2 | quantitative-contraction.tex:318 | |
| info | inferred_dep | outline: "Stated precisions recover F(0) mod 2^p" rests on claim-lem-tapered-hermite-3 | quantitative-contraction.tex:318 | |
| info | inferred_dep | outline: "Polynomial-time rational recombination" rests on claim-lem-tapered-hermite-4 | quantitative-contraction.tex:327 | |
| info | inferred_dep | outline: "Fixed-density bound via contraction theorem" rests on claim-thm-main-1 | quantitative-reduction.tex:86 | |
| info | inferred_dep | outline: "Leaf counts via parity rows and contraction queries" rests on claim-thm-main-3 | quantitative-reduction.tex:330 | |
| info | inferred_dep | outline: "Arbitrary-density time and space accounting" rests on claim-thm-main-3 | quantitative-reduction.tex:347 | |
| info | inferred_dep | outline: "Arbitrary-density time and space accounting" rests on claim-thm-main-4 | quantitative-reduction.tex:347 | |
| info | inferred_dep | outline: "Path length and B-choice bounds" rests on lem:spar-insertion-bound | main_full_version.tex:3809 | |
| info | inferred_dep | outline: "Path length and B-choice bounds" rests on lem:spar-branch | main_full_version.tex:3809 | |
| info | inferred_dep | outline: "Node count via path descriptions" rests on claim-lem-sparsify-2 | main_full_version.tex:3824 | |
| info | inferred_dep | outline: "Choosing M keeps tree within 2^{sigma n}" rests on claim-lem-sparsify-3 | main_full_version.tex:3841 | |
| info | inferred_dep | outline: "Leaf occurrence bound and count partition" rests on claim-lem-sparsify-4 | main_full_version.tex:3855 | |
| info | inferred_dep | outline: "Leaf occurrence bound and count partition" rests on lem:spar-branch | main_full_version.tex:3855 | |
| info | inferred_dep | outline: "Per-node and parameter-search cost" rests on claim-lem-sparsify-4 | main_full_version.tex:3870 |