Where the sources disagree or the structure was guessed, ranked. 107 items · 4 warn · 103 info. In v1 these are paper-internal; Lean-vs-paper rows arrive in Phase 2.
| Severity | Kind | Node | Note | Source |
|---|---|---|---|---|
| warn | unresolved_ref | Final contradiction relies on the external DPRM theorem. | sections/01-introduction.tex:7 | |
| warn | unresolved_ref | The quadratic growth of h(x(nP)) uses canonical height theory cited from Silverman, not a skeleton statement. | sections/02-reduction.tex:755 | |
| warn | unresolved_ref | Finiteness of Sha rests on the external pointwise 2-converse theorem and Cassels-Tate pairing. | sections/03-parity.tex:464 | |
| warn | unresolved_ref | Lower bound rests on the external Green-Tao-Ziegler linear-equations-in-primes theorem. | sections/06-primes.tex:21 | |
| info | inferred_dep | critique: The proof says "Their answers are sound" (02-reduction.tex:884). Soundness of a failed test rests on the integer model of Lemma red:standard-model, as stated at lines 540-543: "an integer zero extends the model of Lemma ". | sections/01-introduction.tex:7 | |
| info | structure_uncertain | The proof environment is a 11-line completion; the actual argument (curve construction, family, CM/non-CM cases, modularity, Jacobian height, isogeny) is spread over unlabeled text throughout Section 4, outlined as claims under hei:height. | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Quaternionic curve quotient is P^1 with five rational branch values" (sections/04-height.tex:43-172) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Abelian surface family with B-action and isogenous conjugates" (sections/04-height.tex:177-280) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "CM fibers have uniformly bounded Faltings height" (sections/04-height.tex:622-680) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Non-CM case: B-linear quasi-isogenies and sign cocycle" (sections/04-height.tex:682-764) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Corrected two-dimensional representation and field L'" (sections/04-height.tex:856-899) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "r_2 is modular from a weight-two newform" (sections/04-height.tex:901-979) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Modular Jacobian height polynomial in N" (sections/04-height.tex:1205-1230) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | structure_uncertain | claim "Faltings height of A polynomial in M via isogeny" (sections/04-height.tex:1232-1297) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:232 | |
| info | inferred_dep | The proof relies on "the nontorsion point P", which Proposition 2.1 provides, to show nonzero multiples avoid O and the two-torsion points. | sections/02-reduction.tex:435 | |
| info | structure_uncertain | Integer-completeness setup (choice of lists, t, twist scaling) lies in unlabeled text between the lemmas of Section 3, outside the short completion proof. | sections/02-reduction.tex:477 | |
| info | structure_uncertain | claim "Choice of fixed multiplier lists M and D_m" (sections/03-parity.tex:108-137) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:477 | |
| info | structure_uncertain | claim "Choice of t making H' locally square at S(m)" (sections/03-parity.tex:139-168) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:477 | |
| info | structure_uncertain | claim "Twist scaling reduces to one parameter n" (sections/03-parity.tex:219-229) lies outside the recorded proof; a second proof or an appendix | sections/02-reduction.tex:477 | |
| info | inferred_dep | critique: The lemma asserts every image element "satisfies Φ" (02-reduction.tex:551-552), and the proof adds "Φ for each term value" (line 564). Φ is the formula of Proposition par:pole-parity, which constraint (d) cites at line 523. | sections/02-reduction.tex:545 | |
| info | inferred_dep | The proof itself cites only the pointwise theorem; Remark 3.5 comes after it and is not used by it. | sections/03-parity.tex:464 | |
| info | inferred_dep | critique: The statement reads "For β,θ,B,J as in Lemma " (03-parity.tex:544). The proof uses at line 568, but the statement itself has no edge. | sections/03-parity.tex:543 | |
| info | inferred_dep | critique: The field L contains "the splitting field K_0 from Lemma " (04-height.tex:575-576). The proof (line 605) uses that K_0 is unramified outside T and that the conjugates have good reduction, both from that lemma. | sections/04-height.tex:584 | |
| info | inferred_dep | critique: Lemma hei:compatibility compares r_3 with "the same algebraic conjugate of f that realizes r_2" (04-height.tex:987-988). This presupposes the modularity identification made in claim-hei-height-6 (lines 952-979). | sections/04-height.tex:986 | |
| info | inferred_dep | The proof repeatedly uses the field L and its uniformly bounded degree ('the uniform upper bound for [L:Q]', 'The uniform local bounds use the bounded degree of L'), which is the field constructed in that lemma. | sections/04-height.tex:1043 | |
| info | inferred_dep | critique: The proof of hei:modular-factor uses that r_2 is realized by the newform f of level N inside V_2(J_1(N)) (04-height.tex:1162-1180). That fact is established in the claim "r_2 is modular from a weight-two newform". | sections/04-height.tex:1170 | |
| info | structure_uncertain | No proof environment; the proof is the prose of sections/06-primes.tex lines 121-699. | sections/06-primes.tex:21 | |
| info | inferred_dep | critique: The statement fixes "a prime r supplied by Lemma " (06-primes.tex:54). The proof (lines 76-78) uses its order conditions gcd(d_1,d_2)|4 and r∤d_1, yet the DAG has no edge. | sections/06-primes.tex:53 | |
| info | inferred_dep | outline: "Image of alpha has exactly eight classes" rests on claim-ell-rank-1 | sections/05-elliptic.tex:55 | |
| info | inferred_dep | outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-1 | sections/05-elliptic.tex:77 | |
| info | inferred_dep | outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-2 | sections/05-elliptic.tex:77 | |
| info | inferred_dep | outline: "Image of alpha' trivial, giving rank one and generator P" rests on claim-ell-rank-3 | sections/05-elliptic.tex:77 | |
| info | inferred_dep | outline: "Coarsened valuation nonnegative on R_F, positive on r" rests on claim-red-coarsening-1 | sections/02-reduction.tex:675 | |
| info | inferred_dep | outline: "Center of coarsened valuation is a tested branch ideal" rests on claim-red-coarsening-2 | sections/02-reduction.tex:685 | |
| info | inferred_dep | outline: "Localization membership transfers to ambient valuation bounds" rests on claim-red-coarsening-3 | sections/02-reduction.tex:700 | |
| info | inferred_dep | outline: "Contact radical K-th power divides delta" rests on claim-red-finite-test-success-1 | sections/02-reduction.tex:792 | |
| info | inferred_dep | outline: "Uniform height bound for all ring elements" rests on claim-red-finite-test-success-2 | sections/02-reduction.tex:816 | |
| info | inferred_dep | outline: "Uniform height bound for all ring elements" rests on hei:height | sections/02-reduction.tex:816 | |
| info | inferred_dep | outline: "Uniform height bound for all ring elements" rests on hei:enlarge-exceptions | sections/02-reduction.tex:816 | |
| info | inferred_dep | outline: "Canonical height comparison bounds root indices" rests on claim-red-finite-test-success-3 | sections/02-reduction.tex:842 | |
| info | inferred_dep | outline: "Root coordinates are ordinary integers" rests on claim-red-finite-test-success-4 | sections/02-reduction.tex:867 | |
| info | inferred_dep | outline: "Local Kummer images at odd primes and at 3" rests on claim-par-descent-1 | sections/03-parity.tex:328 | |
| info | inferred_dep | outline: "Conditions at 2 and real place; normalized Selmer pairs" rests on claim-par-descent-1 | sections/03-parity.tex:359 | |
| info | inferred_dep | outline: "Conditions at 2 and real place; normalized Selmer pairs" rests on claim-par-descent-2 | sections/03-parity.tex:359 | |
| info | inferred_dep | outline: "Selmer conditions as Redei matrix equations" rests on claim-par-descent-3 | sections/03-parity.tex:392 | |
| info | inferred_dep | outline: "Kernel computation bounds Selmer group by eight" rests on claim-par-descent-4 | sections/03-parity.tex:412 | |
| info | inferred_dep | outline: "(beta,1) is a new Selmer class attaining bound" rests on claim-par-descent-5 | sections/03-parity.tex:437 | |
| info | inferred_dep | outline: "(beta,1) is a new Selmer class attaining bound" rests on par:cross-squares | sections/03-parity.tex:437 | |
| info | inferred_dep | outline: "Fixed symbol sums for B and J" rests on par:cross-squares | sections/03-parity.tex:554 | |
| info | inferred_dep | outline: "Auxiliary prime types give required congruences" rests on claim-par-simultaneous-matrices-1 | sections/03-parity.tex:570 | |
| info | inferred_dep | outline: "Matrix target reduces to kernel of K-sharp" rests on claim-par-simultaneous-matrices-2 | sections/03-parity.tex:585 | |
| info | inferred_dep | outline: "Suffices that deleted matrix is nonsingular" rests on claim-par-simultaneous-matrices-3 | sections/03-parity.tex:618 | |
| info | inferred_dep | outline: "Symbol prescription ensures K 1_B = 0" rests on claim-par-simultaneous-matrices-1 | sections/03-parity.tex:627 | |
| info | inferred_dep | outline: "Block matrix M_0 nonsingular on smaller support" rests on claim-par-simultaneous-matrices-5 | sections/03-parity.tex:652 | |
| info | inferred_dep | outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-6 | sections/03-parity.tex:674 | |
| info | inferred_dep | outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-4 | sections/03-parity.tex:674 | |
| info | inferred_dep | outline: "Toggling J diagonal makes enlarged matrix nonsingular" rests on claim-par-simultaneous-matrices-3 | sections/03-parity.tex:674 | |
| info | inferred_dep | outline: "Realize prescribed symbols by Dirichlet primes" rests on claim-par-simultaneous-matrices-7 | sections/03-parity.tex:692 | |
| info | inferred_dep | outline: "Theta-null map height equals Pazuki theta height up to constant" rests on claim-hei-base-height-1 | sections/04-height.tex:405 | |
| info | inferred_dep | outline: "Base height bounded by theta height" rests on claim-hei-base-height-2 | sections/04-height.tex:490 | |
| info | inferred_dep | outline: "Base height bounded by theta height" rests on claim-hei-base-height-3 | sections/04-height.tex:490 | |
| info | inferred_dep | outline: "Pazuki comparison of theta and Faltings heights" rests on claim-hei-base-height-4 | sections/04-height.tex:514 | |
| info | inferred_dep | outline: "Dirichlet character chi matching obstruction class" rests on claim-hei-sign-splitting-1 | sections/04-height.tex:806 | |
| info | inferred_dep | outline: "Order and conductor bounds for chi" rests on claim-hei-sign-splitting-2 | sections/04-height.tex:815 | |
| info | inferred_dep | outline: "Cochain beta splitting epsilon, conjugacy invariant on G_L" rests on claim-hei-sign-splitting-2 | sections/04-height.tex:824 | |
| info | inferred_dep | outline: "Quadratic correction kills inertia outside T" rests on claim-hei-sign-splitting-4 | sections/04-height.tex:835 | |
| info | inferred_dep | outline: "Quadratic correction kills inertia outside T" rests on hei:hom-field | sections/04-height.tex:835 | |
| info | inferred_dep | outline: "Large primes in T are tame with exponent at most two" rests on hei:sign-splitting | sections/04-height.tex:1062 | |
| info | inferred_dep | outline: "Large primes in T are tame with exponent at most two" rests on hei:hom-field | sections/04-height.tex:1062 | |
| info | inferred_dep | outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-1 | sections/04-height.tex:1122 | |
| info | inferred_dep | outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-2 | sections/04-height.tex:1122 | |
| info | inferred_dep | outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-3 | sections/04-height.tex:1122 | |
| info | inferred_dep | outline: "Uniform conductor bound at small primes and N <= CM^2" rests on claim-hei-level-bound-4 | sections/04-height.tex:1122 | |
| info | inferred_dep | outline: "Oracle reduction of integer to rational solvability" rests on red:finite-test-success | sections/07-consequences.tex:26 | |
| info | inferred_dep | outline: "H10(Q) has Turing degree 0'" rests on claim-thm-degree-normal-form-1 | sections/07-consequences.tex:41 | |
| info | inferred_dep | outline: "Many-one reductions to restricted problems give degree 0'" rests on claim-thm-degree-normal-form-2 | sections/07-consequences.tex:87 | |
| info | inferred_dep | outline: "Many-one reductions to restricted problems give degree 0'" rests on claim-thm-degree-normal-form-3 | sections/07-consequences.tex:87 | |
| info | inferred_dep | outline: "Finite multiplier set and initial residue class" rests on claim-pri-pattern-1 | sections/06-primes.tex:184 | |
| info | inferred_dep | outline: "Green-Tao-Ziegler lower bound for prime patterns" rests on claim-pri-pattern-2 | sections/06-primes.tex:318 | |
| info | inferred_dep | outline: "Bound on bad prime values with large common factor" rests on pri:upper-sieve | sections/06-primes.tex:550 | |
| info | inferred_dep | outline: "Bound on bad prime values with large common factor" rests on claim-pri-pattern-4 | sections/06-primes.tex:550 | |
| info | inferred_dep | outline: "Bound on bad prime values with large common factor" rests on claim-pri-pattern-1 | sections/06-primes.tex:550 | |
| info | inferred_dep | outline: "Uniform upper sieve on affine fibers" rests on pri:upper-sieve | sections/06-primes.tex:615 | |
| info | inferred_dep | outline: "Uniform upper sieve on affine fibers" rests on claim-pri-pattern-4 | sections/06-primes.tex:615 | |
| info | inferred_dep | outline: "Surviving prime pattern satisfies order conditions" rests on claim-pri-pattern-3 | sections/06-primes.tex:670 | |
| info | inferred_dep | outline: "Surviving prime pattern satisfies order conditions" rests on claim-pri-pattern-5 | sections/06-primes.tex:670 | |
| info | inferred_dep | outline: "Surviving prime pattern satisfies order conditions" rests on claim-pri-pattern-6 | sections/06-primes.tex:670 | |
| info | inferred_dep | outline: "Surviving prime pattern satisfies order conditions" rests on claim-pri-pattern-1 | sections/06-primes.tex:670 | |
| info | inferred_dep | outline: "Choice of fixed multiplier lists M and D_m" rests on par:soundness | sections/03-parity.tex:108 | |
| info | inferred_dep | outline: "Choice of t making H' locally square at S(m)" rests on claim-par-pole-parity-1 | sections/03-parity.tex:139 | |
| info | inferred_dep | outline: "Twist scaling reduces to one parameter n" rests on par:cross-squares | sections/03-parity.tex:219 | |
| info | inferred_dep | outline: "Abelian surface family with B-action and isogenous conjugates" rests on claim-hei-height-1 | sections/04-height.tex:177 | |
| info | inferred_dep | outline: "CM fibers have uniformly bounded Faltings height" rests on hei:hom-field | sections/04-height.tex:622 | |
| info | inferred_dep | outline: "CM fibers have uniformly bounded Faltings height" rests on hei:base-height | sections/04-height.tex:622 | |
| info | inferred_dep | outline: "CM fibers have uniformly bounded Faltings height" rests on claim-hei-height-2 | sections/04-height.tex:622 | |
| info | inferred_dep | outline: "Non-CM case: B-linear quasi-isogenies and sign cocycle" rests on hei:hom-field | sections/04-height.tex:682 | |
| info | inferred_dep | outline: "Non-CM case: B-linear quasi-isogenies and sign cocycle" rests on claim-hei-height-2 | sections/04-height.tex:682 | |
| info | inferred_dep | outline: "Corrected two-dimensional representation and field L'" rests on claim-hei-height-4 | sections/04-height.tex:856 | |
| info | inferred_dep | outline: "Corrected two-dimensional representation and field L'" rests on hei:sign-splitting | sections/04-height.tex:856 | |
| info | inferred_dep | outline: "r_2 is modular from a weight-two newform" rests on claim-hei-height-5 | sections/04-height.tex:901 | |
| info | inferred_dep | outline: "r_2 is modular from a weight-two newform" rests on hei:sign-splitting | sections/04-height.tex:901 | |
| info | inferred_dep | outline: "r_2 is modular from a weight-two newform" rests on hei:fiber-field | sections/04-height.tex:901 | |
| info | inferred_dep | outline: "Modular Jacobian height polynomial in N" rests on hei:modular-factor | sections/04-height.tex:1205 | |
| info | inferred_dep | outline: "Faltings height of A polynomial in M via isogeny" rests on claim-hei-height-7 | sections/04-height.tex:1232 | |
| info | inferred_dep | outline: "Faltings height of A polynomial in M via isogeny" rests on hei:level-bound | sections/04-height.tex:1232 | |
| info | inferred_dep | outline: "Faltings height of A polynomial in M via isogeny" rests on hei:modular-factor | sections/04-height.tex:1232 | |
| info | inferred_dep | outline: "Faltings height of A polynomial in M via isogeny" rests on claim-hei-height-5 | sections/04-height.tex:1232 |