Where the sources disagree or the structure was guessed, ranked. 83 items · 3 warn · 80 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 on the external Khot–Minzer–Safra Grassmann expansion theorem (cited, not a skeleton statement). | sections/04-matrix.tex:33 | |
| warn | unresolved_ref | Bound on influential coordinates per right vertex is imported from Guruswami et al. Lemma 4.3. | appendices/finite-consequences.tex:242 | |
| warn | unresolved_ref | Key step is the external vector-valued invariance theorem (Guruswami et al. Thm 10.1 / Isaksson–Mossel). | appendices/finite-consequences.tex:515 | |
| info | inferred_dep | critique: The proof of Lemma 3.1 uses Eq. (latent-base-detection) at sections/02-latent.tex:739-740. That equation is derived in running text from "Proposition gives the bound" (line 653). The lemma node has no edge to the proposition. | sections/02-latent.tex:8 | |
| info | inferred_dep | The proof verifies the "nonproportionality condition" and "alignment condition", which are the two parts of the definition of a generic subspace. | sections/02-latent.tex:256 | |
| info | structure_uncertain | The base detection bound (eq. latent-base-detection) deriving from this proposition is argued in running text (lines 639-654) outside any proof environment, then used in the proof of lem:latent. | sections/02-latent.tex:534 | |
| info | structure_uncertain | No proof in paper; imported from Håstad's Theorem 5.4. | sections/03-game.tex:25 | |
| info | inferred_dep | critique: Proposition 5.3 concludes that "the projected advice experiment with β=k^{-2/3} has local strategies" (sections/04-matrix.tex:220-222). That experiment is exactly Definition 5.2. | sections/04-matrix.tex:197 | |
| info | inferred_dep | the proof refers to "the ordinary shortcode equality tests" at fixed (U,T), which are the tests of the inverse shortcode theorem | sections/04-matrix.tex:244 | |
| info | inferred_dep | critique: The statement of Lemma 5.7 (sections/04-matrix.tex:552) says "of the joint data D in Definition ". The definition is currently flagged as an orphan. | sections/04-matrix.tex:543 | |
| info | inferred_dep | critique: The statement of Lemma 5.8 (sections/04-matrix.tex:678) begins "Fix joint data satisfying Lemma ". This dependency exists only on a child claim, not on the lemma node itself. | sections/04-matrix.tex:676 | |
| info | structure_uncertain | No proof in paper; it is Dinur–Steurer Corollary 1.2. | sections/05-clean.tex:26 | |
| info | inferred_dep | critique: Lemma 6.2 bounds agreement "in the advice experiment". Its proof setup (sections/05-clean.tex:66-86) recalls the advice experiment of Section 5, which is Definition 5.2. | sections/05-clean.tex:88 | |
| info | inferred_dep | critique: The proof (sections/07-consequences.tex:92-94, 117-119) uses "the formulation above" and "the nonempty simple game supplied above". That formulation is Lemma A.1, introduced at lines 55-62. The edge exists only on child claims. | sections/07-consequences.tex:64 | |
| info | inferred_dep | The proof uses the Gram data and the atom bound α, which are supplied by Lemma A.3 ("the data of Lemma "); that reference sits in the statement, not as a linked \ref. | appendices/finite-consequences.tex:515 | |
| info | inferred_dep | outline: "Alphabet-independent gap fixes repetition exponent" rests on lem:unweighted-subdivision | sections/06-finish.tex:93 | |
| info | inferred_dep | outline: "Choosing the cube k and parity error" rests on lem:projected-tv | sections/06-finish.tex:136 | |
| info | inferred_dep | outline: "Choosing the cube k and parity error" rests on lem:clean | sections/06-finish.tex:136 | |
| info | inferred_dep | outline: "Choosing the cube k and parity error" rests on claim-thm-ugc-2 | sections/06-finish.tex:136 | |
| info | inferred_dep | outline: "YES and NO values of the final game" rests on thm:repetition | sections/06-finish.tex:176 | |
| info | inferred_dep | outline: "YES and NO values of the final game" rests on claim-thm-ugc-1 | sections/06-finish.tex:176 | |
| info | inferred_dep | outline: "YES and NO values of the final game" rests on claim-thm-ugc-3 | sections/06-finish.tex:176 | |
| info | inferred_dep | outline: "Output is simple bipartite translation game" rests on lem:unweighted-subdivision | sections/06-finish.tex:204 | |
| info | inferred_dep | outline: "Polynomial-time explicit encoding" rests on lem:unweighted-subdivision | sections/06-finish.tex:216 | |
| info | inferred_dep | outline: "Enlarged noise preserves small change probability" rests on claim-lem-latent-1 | sections/02-latent.tex:701 | |
| info | inferred_dep | outline: "Enlarged noise preserves small change probability" rests on claim-lem-latent-2 | sections/02-latent.tex:701 | |
| info | inferred_dep | outline: "High-rank families restrict onto B and detect" rests on prop:latent-full-lift-detection | sections/02-latent.tex:711 | |
| info | inferred_dep | outline: "High-rank families restrict onto B and detect" rests on claim-lem-latent-2 | sections/02-latent.tex:711 | |
| info | inferred_dep | outline: "Generic non-membership over function field" rests on claim-lem-latent-generic-2 | sections/02-latent.tex:294 | |
| info | inferred_dep | outline: "Specialization via polynomial zero bound" rests on claim-lem-latent-generic-1 | sections/02-latent.tex:337 | |
| info | inferred_dep | outline: "Specialization via polynomial zero bound" rests on claim-lem-latent-generic-3 | sections/02-latent.tex:337 | |
| info | inferred_dep | outline: "Fresh isomorphisms make genericity typical" rests on lem:latent-generic | sections/02-latent.tex:547 | |
| info | inferred_dep | outline: "Fresh isomorphisms make genericity typical" rests on lem:latent-lift-factorization | sections/02-latent.tex:547 | |
| info | inferred_dep | outline: "Expected harmonic rank drop per level" rests on lem:latent-block-kernel | sections/02-latent.tex:579 | |
| info | inferred_dep | outline: "Expected harmonic rank drop per level" rests on claim-prop-latent-full-lift-detection-1 | sections/02-latent.tex:579 | |
| info | inferred_dep | outline: "Rank survives with probability half, leaf detection" rests on claim-prop-latent-full-lift-detection-2 | sections/02-latent.tex:600 | |
| info | inferred_dep | outline: "Matrix chart lift has Grassmann retention eta/4" rests on claim-thm-shortcode-1 | sections/04-matrix.tex:88 | |
| info | inferred_dep | outline: "Expansion interval yields row-column slice" rests on claim-thm-shortcode-2 | sections/04-matrix.tex:109 | |
| info | inferred_dep | outline: "Shortcode contradiction forces large good set" rests on claim-lem-good-row-advice-1 | sections/04-matrix.tex:396 | |
| info | inferred_dep | outline: "Shortcode contradiction forces large good set" rests on claim-lem-good-row-advice-2 | sections/04-matrix.tex:396 | |
| info | inferred_dep | outline: "Lower bound g_0 on good advice mass" rests on claim-lem-good-row-advice-3 | sections/04-matrix.tex:407 | |
| info | inferred_dep | outline: "Slice correlation with nontrivial restriction" rests on lem:projected-witness | sections/04-matrix.tex:688 | |
| info | inferred_dep | outline: "Fourier mass on indicated frequency coset" rests on claim-lem-fourier-coset-decoding-1 | sections/04-matrix.tex:712 | |
| info | inferred_dep | outline: "Decoded vector lands in projected answer set" rests on claim-lem-fourier-coset-decoding-2 | sections/04-matrix.tex:737 | |
| info | inferred_dep | outline: "Decoded vector lands in projected answer set" rests on lem:good-row-advice | sections/04-matrix.tex:737 | |
| info | inferred_dep | outline: "Clean coordinates have ordinary question law" rests on claim-lem-clean-1 | sections/05-clean.tex:123 | |
| info | inferred_dep | outline: "Conditioned clean pairs are independent game questions" rests on claim-lem-clean-2 | sections/05-clean.tex:141 | |
| info | inferred_dep | outline: "Each side reconstructs its advice input" rests on claim-lem-clean-3 | sections/05-clean.tex:167 | |
| info | inferred_dep | outline: "Conditional agreement bounded by repeated game" rests on claim-lem-clean-4 | sections/05-clean.tex:202 | |
| info | inferred_dep | outline: "Averaging over binomial clean count" rests on claim-lem-clean-5 | sections/05-clean.tex:223 | |
| info | inferred_dep | outline: "Averaging over binomial clean count" rests on claim-lem-clean-2 | sections/05-clean.tex:223 | |
| info | inferred_dep | outline: "Fixed-instance verifier gap from strong-left UG" rests on lem:simple-strong-left | sections/07-consequences.tex:89 | |
| info | inferred_dep | outline: "Fixed-instance verifier gap from strong-left UG" rests on claim-cor-raghavendra-consequence-1 | sections/07-consequences.tex:89 | |
| info | inferred_dep | outline: "Rational approximation of local law" rests on claim-cor-raghavendra-consequence-2 | sections/07-consequences.tex:98 | |
| info | inferred_dep | outline: "Explicit polynomial occurrence list" rests on lem:simple-strong-left | sections/07-consequences.tex:117 | |
| info | inferred_dep | outline: "Explicit polynomial occurrence list" rests on claim-cor-raghavendra-consequence-3 | sections/07-consequences.tex:117 | |
| info | inferred_dep | outline: "Rationalization changes optimum by under eta/2" rests on claim-cor-raghavendra-consequence-2 | sections/07-consequences.tex:145 | |
| info | inferred_dep | outline: "Rationalization changes optimum by under eta/2" rests on claim-cor-raghavendra-consequence-3 | sections/07-consequences.tex:145 | |
| info | inferred_dep | outline: "Rationalization changes optimum by under eta/2" rests on claim-cor-raghavendra-consequence-4 | sections/07-consequences.tex:145 | |
| info | inferred_dep | outline: "Copy normalization to unit incident weight" rests on claim-lem-simple-strong-left-1 | appendices/finite-consequences.tex:69 | |
| info | inferred_dep | outline: "Copy normalization to unit incident weight" rests on thm:ugc | appendices/finite-consequences.tex:69 | |
| info | inferred_dep | outline: "Rounding weights into unweighted multigraph" rests on claim-lem-simple-strong-left-2 | appendices/finite-consequences.tex:103 | |
| info | inferred_dep | outline: "Tagged right copies preserve value" rests on claim-lem-simple-strong-left-3 | appendices/finite-consequences.tex:124 | |
| info | inferred_dep | outline: "Full sequence graph value below 3nu/4" rests on claim-lem-simple-strong-left-4 | appendices/finite-consequences.tex:142 | |
| info | inferred_dep | outline: "Distinct-tag graph simple, YES strongly satisfied" rests on claim-lem-simple-strong-left-3 | appendices/finite-consequences.tex:184 | |
| info | inferred_dep | outline: "Distinct-tag graph simple, YES strongly satisfied" rests on claim-lem-simple-strong-left-4 | appendices/finite-consequences.tex:184 | |
| info | inferred_dep | outline: "NO soundness of retained graph" rests on claim-lem-simple-strong-left-5 | appendices/finite-consequences.tex:210 | |
| info | inferred_dep | outline: "NO soundness of retained graph" rests on claim-lem-simple-strong-left-6 | appendices/finite-consequences.tex:210 | |
| info | inferred_dep | outline: "Construction is polynomial size" rests on claim-lem-simple-strong-left-6 | appendices/finite-consequences.tex:221 | |
| info | inferred_dep | outline: "Pseudorandom vertices have local payoff bound" rests on claim-prop-finite-ordering-transfer-2 | appendices/finite-consequences.tex:737 | |
| info | inferred_dep | outline: "Nonpseudorandom excess decodes to game labeling" rests on claim-prop-finite-ordering-transfer-3 | appendices/finite-consequences.tex:805 | |
| info | inferred_dep | outline: "Nonpseudorandom excess decodes to game labeling" rests on claim-prop-finite-ordering-transfer-4 | appendices/finite-consequences.tex:805 | |
| info | inferred_dep | outline: "Conditioning on distinct neighbors gives strict gap" rests on claim-prop-finite-ordering-transfer-1 | appendices/finite-consequences.tex:852 | |
| info | inferred_dep | outline: "Conditioning on distinct neighbors gives strict gap" rests on claim-prop-finite-ordering-transfer-5 | appendices/finite-consequences.tex:852 | |
| info | inferred_dep | outline: "Parameter choices give final ordering gap" rests on lem:ordering-collision | appendices/finite-consequences.tex:904 | |
| info | inferred_dep | outline: "Parameter choices give final ordering gap" rests on lem:ordering-rounding | appendices/finite-consequences.tex:904 | |
| info | inferred_dep | outline: "Parameter choices give final ordering gap" rests on claim-prop-finite-ordering-transfer-6 | appendices/finite-consequences.tex:904 | |
| info | inferred_dep | outline: "Explicit rational encoding is polynomial" rests on claim-prop-finite-ordering-transfer-6 | appendices/finite-consequences.tex:945 | |
| info | inferred_dep | outline: "Common Gaussian ensemble matching local moments" rests on lem:ordering-local-data | appendices/finite-consequences.tex:557 | |
| info | inferred_dep | outline: "Influence and tail hypotheses for invariance" rests on claim-lem-ordering-rounding-1 | appendices/finite-consequences.tex:576 | |
| info | inferred_dep | outline: "Lipschitz payoff gives R-independent invariance error" rests on claim-lem-ordering-rounding-2 | appendices/finite-consequences.tex:623 | |
| info | inferred_dep | outline: "Lipschitz payoff gives R-independent invariance error" rests on claim-lem-ordering-rounding-3 | appendices/finite-consequences.tex:623 | |
| info | inferred_dep | outline: "Gaussian side is a random q-assignment" rests on claim-lem-ordering-rounding-4 | appendices/finite-consequences.tex:642 |