TauLib · API Book III

TauLib.BookIII.Arithmetic.BSD

TauLib.BookIII.Arithmetic.BSD

BSD Coherence Theorem and BSD Three-Ingredient Proof.

Registry Cross-References

  • [III.T35] BSD Coherence Theorem – bsd_coherence_check

  • [III.P27] BSD Three-Ingredient Proof – bsd_three_ingredient_check

Mathematical Content

III.T35 (BSD Coherence): For τ-admissible elliptic data, BSD_τ(k) stabilizes and equals the rank of the τ-rational point group. The functional encodes the analytic rank (L-value derivative) and the algebraic rank (tower depth).

III.P27 (BSD Three-Ingredient Proof): BSD coherence follows from three ingredients: (1) rank stabilization at finite depth, (2) L-value stabilization via primorial cofinality, (3) E₁ Mutual Determination equality.


Tau.BookIII.Arithmetic.bsd_coherence_check

source def Tau.BookIII.Arithmetic.bsd_coherence_check (db : Denotation.TauIdx) :Bool

[III.T35] BSD coherence: the BSD functional stabilizes across depths. BSD_τ(k) at k is compatible with BSD_τ(k+1) at k+1. Equations

  • Tau.BookIII.Arithmetic.bsd_coherence_check db = Tau.BookIII.Arithmetic.bsd_coherence_check.go db 1 (db + 1) Instances For

Tau.BookIII.Arithmetic.bsd_coherence_check.go

source@[irreducible]

**def Tau.BookIII.Arithmetic.bsd_coherence_check.go (db : Denotation.TauIdx)

(k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Arithmetic.bsd_rank_agreement_check

source def Tau.BookIII.Arithmetic.bsd_rank_agreement_check (db : Denotation.TauIdx) :Bool

[III.T35] BSD functional-rank agreement: the BSD functional at level k is related to the number of stabilized rational points. Equations

  • Tau.BookIII.Arithmetic.bsd_rank_agreement_check db = Tau.BookIII.Arithmetic.bsd_rank_agreement_check.go db 0 1 (db + 1) Instances For

Tau.BookIII.Arithmetic.bsd_rank_agreement_check.go

source@[irreducible]

**def Tau.BookIII.Arithmetic.bsd_rank_agreement_check.go (db : Denotation.TauIdx)

(dummy k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Arithmetic.bsd_rank_agreement_check.check_all_rational

source@[irreducible]

def Tau.BookIII.Arithmetic.bsd_rank_agreement_check.check_all_rational (x pk k fuel2 : ℕ) :Bool

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Arithmetic.bsd_three_ingredient_check

source def Tau.BookIII.Arithmetic.bsd_three_ingredient_check (bound db : Denotation.TauIdx) :Bool

[III.P27] BSD three-ingredient proof: (1) Rank stabilization: ranks are bounded (2) L-value stabilization: split-zeta products stabilize (3) E₁ MD equality: boundary determines interior determines spectral Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Arithmetic.bsd_three_ingredient_check.l_value_stab_go

source@[irreducible]

def Tau.BookIII.Arithmetic.bsd_three_ingredient_check.l_value_stab_go (k db fuel : ℕ) :Bool

L-value stabilization: B and C products at k divide those at k+1. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookIII.Arithmetic.bsd_coherence_5

source theorem Tau.BookIII.Arithmetic.bsd_coherence_5 :bsd_coherence_check 5 = true


Tau.BookIII.Arithmetic.bsd_rank_agreement_4

source theorem Tau.BookIII.Arithmetic.bsd_rank_agreement_4 :bsd_rank_agreement_check 4 = true


Tau.BookIII.Arithmetic.bsd_three_ingredient_15_3

source theorem Tau.BookIII.Arithmetic.bsd_three_ingredient_15_3 :bsd_three_ingredient_check 15 3 = true


Tau.BookIII.Arithmetic.bsd_coherence_1

source theorem Tau.BookIII.Arithmetic.bsd_coherence_1 :bsd_coherence_check 1 = true

[III.T35] Structural: BSD coherence at depth 1.


Tau.BookIII.Arithmetic.bsd_level

source theorem Tau.BookIII.Arithmetic.bsd_level :Doors.problem_level Doors.MillenniumProblem.BSD = Enrichment.EnrLevel.E2

[III.P27] Structural: BSD is at E₁→E₂ interface.


Tau.BookIII.Arithmetic.bsd_part

source theorem Tau.BookIII.Arithmetic.bsd_part :Doors.problem_part Doors.MillenniumProblem.BSD = 6