Where the sources disagree or the structure was guessed, ranked. 88 items · 2 warn · 86 info. In v1 these are paper-internal; Lean-vs-paper rows arrive in Phase 2.
| Severity | Kind | Node | Note | Source |
|---|---|---|---|---|
| warn | unresolved_ref | Choice of d_0 relies on equation ht:independent-profiles (Tonelli/height identity), not a skeleton statement. | sections/03-heights.tex:216 | |
| warn | unresolved_ref | Excluding b=1 uses the unit-circle exclusion equation alg:unit-circle and deletion hypothesis argued in Section 8 text, not a labeled statement. | sections/07-algebra.tex:438 | |
| info | inferred_dep | "the sequence reduction in " giving configurations with t^{4-o(1)} ordered unit pairs, and "the incidence pieces used throughout the proof" | sections/00-introduction.tex:12 | |
| info | inferred_dep | The proof invokes ('the incidence bound') for the edge upper bound, the degree deletions and the preliminary expansion; that equation is the bound of Proposition 2.3. | sections/01-incidence.tex:176 | |
| info | inferred_dep | critique: Lemma inc:matching is "For the sequence of edge laws in " (01-incidence.tex:357) and its proof sums and uses . | sections/01-incidence.tex:356 | |
| info | inferred_dep | critique: Lemma inc:rare's proof (01-incidence.tex:454-473) follows from , derived from Proposition inc:piece. | sections/01-incidence.tex:424 | |
| info | inferred_dep | critique: 01-incidence.tex:518 proves the atom estimate "by --", which are the conclusions of Proposition inc:piece. | sections/01-incidence.tex:493 | |
| info | inferred_dep | critique: Corollary pred:acceptance is stated "In the setting of " (02-prediction.tex:186) and its proof averages (line 208). | sections/02-prediction.tex:185 | |
| info | inferred_dep | The proof invokes the normalized extensions and the "product formula" for the height, which is the weighted product formula of Lemma 4.1 (). | sections/03-heights.tex:73 | |
| info | inferred_dep | critique: 04-budgets.tex:433-434: "The integrals of the joint terms I_xI_{y_j} are o(S) by ", from Lemma bud:rare-moments. | sections/04-budgets.tex:404 | |
| info | structure_uncertain | Proof uses com:ghost via eq. com:mixture and the bad-mass estimate, though the skeleton refs list only com:transfer; ext:band likewise uses ext:profiles via equation refs. | sections/05-common-levels.tex:246 | |
| info | inferred_dep | "As before, a pair with a bad slot costs only O(b_p)" and "The strict-cross classification proves the claim" point back to the classification of common variation in §6.2. | sections/05-common-levels.tex:437 | |
| info | inferred_dep | critique: 06-extraction.tex:231: "the first term averages to C_Q=o(S)", which is of Proposition com:variation. | sections/06-extraction.tex:199 | |
| info | inferred_dep | critique: Proof of ext:band (06-extraction.tex:278-308) sets Z=E_1+E_2 from Lemma ext:profiles and uses at line 306, but the DAG has no edge. | sections/06-extraction.tex:262 | |
| info | inferred_dep | critique: 06-extraction.tex:443 "By and " uses the profile approximation of Lemma ext:profiles to bound b_{pr}. | sections/06-extraction.tex:379 | |
| info | structure_uncertain | No proof environment; proved by the running text of Section 8 (lines 40-678), assembling Lemmas 8.2-8.6, ending with 'This proves Proposition alg:obstruction'. | sections/07-algebra.tex:14 | |
| info | inferred_dep | the weighted product formula over the absolute values, 'total weight of the infinite places is one', and the use of h(u) rely on the product formula of §4.1 | sections/07-algebra.tex:78 | |
| info | inferred_dep | 'These statements do not depend on representatives' refers to h(u) being independent of the chosen normal field and extensions | sections/07-algebra.tex:78 | |
| info | inferred_dep | critique: 07-algebra.tex:412-413: "The function-field assertion is the evaluation argument following ", i.e. lines 293-310 (claim-alg-obstruction-3). | sections/07-algebra.tex:395 | |
| info | inferred_dep | outline: "Sweep pieces avoid sampled circles, cover points" rests on claim-inc-cutting-1 | sections/01-incidence.tex:98 | |
| info | inferred_dep | outline: "Number of pieces is O(1+s^2)" rests on claim-inc-cutting-2 | sections/01-incidence.tex:117 | |
| info | inferred_dep | outline: "Conflict bound via union over candidate regions" rests on claim-inc-cutting-2 | sections/01-incidence.tex:129 | |
| info | inferred_dep | outline: "Some small piece carries many incidences" rests on claim-inc-piece-1 | sections/01-incidence.tex:221 | |
| info | inferred_dep | outline: "Some small piece carries many incidences" rests on inc:incidence | sections/01-incidence.tex:221 | |
| info | inferred_dep | outline: "Trimming high-degree vertices gives degree bounds" rests on claim-inc-piece-2 | sections/01-incidence.tex:234 | |
| info | inferred_dep | outline: "Trimming high-degree vertices gives degree bounds" rests on inc:incidence | sections/01-incidence.tex:234 | |
| info | inferred_dep | outline: "Preliminary square-root expansion bound" rests on claim-inc-piece-3 | sections/01-incidence.tex:254 | |
| info | inferred_dep | outline: "Preliminary square-root expansion bound" rests on inc:incidence | sections/01-incidence.tex:254 | |
| info | inferred_dep | outline: "Density-maximizing rectangle retains large fractions" rests on claim-inc-piece-4 | sections/01-incidence.tex:273 | |
| info | inferred_dep | outline: "Expansion estimate from optimality of rectangle" rests on claim-inc-piece-4 | sections/01-incidence.tex:303 | |
| info | inferred_dep | outline: "Expansion estimate from optimality of rectangle" rests on claim-inc-piece-5 | sections/01-incidence.tex:303 | |
| info | inferred_dep | outline: "Marginal atom lower bounds by vertex removal" rests on claim-inc-piece-5 | sections/01-incidence.tex:327 | |
| info | inferred_dep | outline: "Residual inner products have small average" rests on claim-pred-device-1 | sections/02-prediction.tex:138 | |
| info | inferred_dep | outline: "Wedge square identity bounds center discrepancy" rests on claim-pred-device-2 | sections/02-prediction.tex:154 | |
| info | inferred_dep | outline: "Replace step test by fresh test; fix history" rests on claim-pred-device-3 | sections/02-prediction.tex:167 | |
| info | inferred_dep | outline: "Coupling tail bounds uniform in history" rests on claim-ht-bounded-1 | sections/03-heights.tex:250 | |
| info | inferred_dep | outline: "Coupling tail bounds uniform in history" rests on ht:height | sections/03-heights.tex:250 | |
| info | inferred_dep | outline: "Positive-probability outcome: tests pass, separated" rests on claim-ht-bounded-2 | sections/03-heights.tex:307 | |
| info | inferred_dep | outline: "Positive-probability outcome: tests pass, separated" rests on claim-ht-bounded-3 | sections/03-heights.tex:307 | |
| info | inferred_dep | outline: "Determinant and Cramer's rule contradiction" rests on claim-ht-bounded-4 | sections/03-heights.tex:330 | |
| info | inferred_dep | outline: "Place identity; positive charges in flanking intervals" rests on ht:states | sections/04-budgets.tex:301 | |
| info | inferred_dep | outline: "Rare positives lie on one side only" rests on claim-bud-upper-1 | sections/04-budgets.tex:335 | |
| info | inferred_dep | outline: "Central-window excess and product-formula cancellation" rests on claim-bud-upper-1 | sections/04-budgets.tex:345 | |
| info | inferred_dep | outline: "Central-window excess and product-formula cancellation" rests on claim-bud-upper-2 | sections/04-budgets.tex:345 | |
| info | inferred_dep | outline: "Central-window excess and product-formula cancellation" rests on ht:product | sections/04-budgets.tex:345 | |
| info | inferred_dep | outline: "Averaging bounds distinct pairs by 10δ²λC_i" rests on claim-bud-upper-3 | sections/04-budgets.tex:367 | |
| info | inferred_dep | outline: "Averaging bounds distinct pairs by 10δ²λC_i" rests on bud:intervals | sections/04-budgets.tex:367 | |
| info | inferred_dep | outline: "Slice score lower bound by strict-cross classification" rests on claim-com-variation-1 | sections/05-common-levels.tex:285 | |
| info | inferred_dep | outline: "Slice score lower bound by strict-cross classification" rests on com:transfer | sections/05-common-levels.tex:285 | |
| info | inferred_dep | outline: "Slice score lower bound by strict-cross classification" rests on com:ghost | sections/05-common-levels.tex:285 | |
| info | inferred_dep | outline: "Comparing budgets gives C_Q+C_Pθ=o(S)" rests on claim-com-variation-2 | sections/05-common-levels.tex:329 | |
| info | inferred_dep | outline: "Center rare exceptions bounded by point ones" rests on claim-com-variation-3 | sections/05-common-levels.tex:349 | |
| info | inferred_dep | outline: "Assumption forces center exceptions and T small" rests on com:variation | sections/05-common-levels.tex:445 | |
| info | inferred_dep | outline: "Pointwise point-star slice inequality" rests on claim-com-rare-positive-1 | sections/05-common-levels.tex:450 | |
| info | inferred_dep | outline: "Point-star common variation C_P=o(S)" rests on claim-com-rare-positive-2 | sections/05-common-levels.tex:517 | |
| info | inferred_dep | outline: "Point-star common variation C_P=o(S)" rests on bud:upper | sections/05-common-levels.tex:517 | |
| info | inferred_dep | outline: "Small star variations force small f on common levels" rests on claim-com-rare-positive-3 | sections/05-common-levels.tex:533 | |
| info | inferred_dep | outline: "Small star variations force small f on common levels" rests on com:variation | sections/05-common-levels.tex:533 | |
| info | inferred_dep | outline: "Rare levels small too, contradiction S=o(S)" rests on claim-com-rare-positive-4 | sections/05-common-levels.tex:550 | |
| info | inferred_dep | outline: "Capped pointwise inequality on the tail set" rests on ext:pointwise | sections/06-extraction.tex:107 | |
| info | inferred_dep | outline: "Averaging over neighbor pairs" rests on claim-ext-tail-1 | sections/06-extraction.tex:130 | |
| info | inferred_dep | outline: "Layer-cake expansion bound on capped expectation" rests on inc:piece | sections/06-extraction.tex:142 | |
| info | inferred_dep | outline: "Young's inequality absorbs tail moment" rests on claim-ext-tail-2 | sections/06-extraction.tex:173 | |
| info | inferred_dep | outline: "Young's inequality absorbs tail moment" rests on claim-ext-tail-3 | sections/06-extraction.tex:173 | |
| info | inferred_dep | outline: "Power saving for vanishing tests by induction" rests on claim-alg-generic-grid-1 | sections/07-algebra.tex:244 | |
| info | inferred_dep | outline: "Diagonal grid choice avoids all countable tests" rests on claim-alg-generic-grid-2 | sections/07-algebra.tex:265 | |
| info | inferred_dep | outline: "Diagonal grid choice avoids all countable tests" rests on claim-alg-generic-grid-3 | sections/07-algebra.tex:265 | |
| info | inferred_dep | outline: "Curve coordinates algebraic; transcendence conclusions" rests on claim-alg-generic-grid-4 | sections/07-algebra.tex:279 | |
| info | inferred_dep | outline: "Curve case: simple point s_ell off anchor" rests on alg:generic-grid | sections/07-algebra.tex:467 | |
| info | inferred_dep | outline: "Other radicands nonvanishing at s_ell" rests on claim-alg-private-valuations-2 | sections/07-algebra.tex:489 | |
| info | inferred_dep | outline: "Other radicands nonvanishing at s_ell" rests on alg:generic-grid | sections/07-algebra.tex:489 | |
| info | inferred_dep | outline: "Power-series embedding gives order-one valuation" rests on claim-alg-private-valuations-2 | sections/07-algebra.tex:510 | |
| info | inferred_dep | outline: "Power-series embedding gives order-one valuation" rests on claim-alg-private-valuations-3 | sections/07-algebra.tex:510 | |
| info | inferred_dep | outline: "Line case private simple zero" rests on claim-alg-private-valuations-5 | sections/07-algebra.tex:546 | |
| info | inferred_dep | outline: "Fractional-linear case private simple zero" rests on claim-alg-private-valuations-5 | sections/07-algebra.tex:560 | |
| info | inferred_dep | outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-1 | sections/07-algebra.tex:587 | |
| info | inferred_dep | outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-4 | sections/07-algebra.tex:587 | |
| info | inferred_dep | outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-6 | sections/07-algebra.tex:587 | |
| info | inferred_dep | outline: "Odd valuations give square-class independence" rests on claim-alg-private-valuations-7 | sections/07-algebra.tex:587 | |
| info | inferred_dep | outline: "Ratios transcendental, rectangle defects in k0" rests on alg:small-height-field | sections/07-algebra.tex:109 | |
| info | inferred_dep | outline: "Generic points embed function fields" rests on claim-alg-obstruction-2 | sections/07-algebra.tex:293 | |
| info | inferred_dep | outline: "Generic points embed function fields" rests on alg:generic-grid | sections/07-algebra.tex:293 | |
| info | inferred_dep | outline: "Grid ratios factor through k0 defects" rests on claim-alg-obstruction-1 | sections/07-algebra.tex:314 | |
| info | inferred_dep | outline: "Grid ratios factor through k0 defects" rests on alg:generic-grid | sections/07-algebra.tex:314 | |
| info | inferred_dep | outline: "Differentiated linear system with radicals" rests on claim-alg-obstruction-4 | sections/07-algebra.tex:356 | |
| info | inferred_dep | outline: "Differentiated linear system with radicals" rests on alg:derivation | sections/07-algebra.tex:356 | |
| info | inferred_dep | outline: "Unused sign change contradicts nonzero derivative" rests on claim-alg-obstruction-5 | sections/07-algebra.tex:605 | |
| info | inferred_dep | outline: "Unused sign change contradicts nonzero derivative" rests on alg:surviving-point | sections/07-algebra.tex:605 |