TauLib · API Book III

TauLib.BookIII.Arithmetic.Langlands

TauLib.BookIII.Arithmetic.Langlands

Automorphic-Galois Duality, Local Langlands Instance, Duality as MD on ℤ², Functoriality Theorem, and Base Change-Transfer Naturality.

Registry Cross-References

  • [III.D63] Automorphic-Galois Duality – ag_duality_check

  • [III.D64] Local Langlands Instance – local_langlands_check

  • [III.P28] Duality as Mutual Determination on ℤ² – duality_md_check

  • [III.T36] Functoriality Theorem – functoriality_check

  • [III.T37] Base Change-Transfer Naturality – base_change_check

Mathematical Content

III.D63 (Automorphic-Galois Duality): Bidirectional correspondence between m-axis (Galois/prime) and n-axis (automorphic/spectral) data on ℤ².

III.D64 (Local Langlands Instance): At each prime p, the matched pair (Fr_p, λ_p) with Frobenius equals spectral character restricted to m-axis.

III.P28 (Duality as MD on ℤ²): The A-G duality IS Mutual Determination with m-axis as boundary, n-axis as spectral, full character as interior.

III.T36 (Functoriality): For every sector morphism f: S₁→S₂, the induced map on boundary characters commutes with spectral decomposition.

III.T37 (Base Change-Transfer): Base change and transfer are natural transformations on the enriched bi-square.

Tau.BookIII.Arithmetic.ag_duality_check

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

[III.D63] Automorphic-Galois duality on ℤ² at finite level: m-axis (Galois) = B-part of BNF, n-axis (automorphic) = C-part. The duality maps m-data to n-data and vice versa. Equations

  • Tau.BookIII.Arithmetic.ag_duality_check bound db = Tau.BookIII.Arithmetic.ag_duality_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Arithmetic.ag_duality_check.go

source@[irreducible]

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

(x k fuel : ℕ) :Bool**

Equations

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

Tau.BookIII.Arithmetic.local_langlands_check

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

[III.D64] Local Langlands at prime p: the Frobenius at p is encoded by the BNF component at the p-th prime position. The spectral character restricted to the m-axis gives the Frobenius eigenvalue. Equations

  • Tau.BookIII.Arithmetic.local_langlands_check bound db = Tau.BookIII.Arithmetic.local_langlands_check.go bound db 1 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Arithmetic.local_langlands_check.go

source@[irreducible]

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

(i k fuel : ℕ) :Bool**

Equations

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

Tau.BookIII.Arithmetic.duality_md_check

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

[III.P28] Duality as Mutual Determination: the A-G duality IS MD with m-axis = boundary, n-axis = spectral, full = interior. Equations

  • Tau.BookIII.Arithmetic.duality_md_check bound db = Tau.BookIII.Arithmetic.duality_md_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Arithmetic.duality_md_check.go

source@[irreducible]

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

(x k fuel : ℕ) :Bool**

Equations

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

Tau.BookIII.Arithmetic.functoriality_check

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

[III.T36] Functoriality: sector morphisms (BNF-preserving maps) commute with spectral decomposition. At finite level: the polarity swap commutes with the B/C/X decomposition. Equations

  • Tau.BookIII.Arithmetic.functoriality_check bound db = Tau.BookIII.Arithmetic.functoriality_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Arithmetic.functoriality_check.go

source@[irreducible]

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

(x k fuel : ℕ) :Bool**

Equations

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

Tau.BookIII.Arithmetic.base_change_check

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

[III.T37] Base change-transfer naturality: the enrichment functor Enr₀₁ on sector morphisms and the defect functional between sectors are natural transformations. Checked by: tower projection commutes with sector decomposition. Equations

  • Tau.BookIII.Arithmetic.base_change_check bound db = Tau.BookIII.Arithmetic.base_change_check.go bound db 0 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookIII.Arithmetic.base_change_check.go

source@[irreducible]

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

(x k fuel : ℕ) :Bool**

Equations

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

Tau.BookIII.Arithmetic.ag_duality_15_4

source theorem Tau.BookIII.Arithmetic.ag_duality_15_4 :ag_duality_check 15 4 = true

Tau.BookIII.Arithmetic.local_langlands_10_3

source theorem Tau.BookIII.Arithmetic.local_langlands_10_3 :local_langlands_check 10 3 = true

Tau.BookIII.Arithmetic.duality_md_15_4

source theorem Tau.BookIII.Arithmetic.duality_md_15_4 :duality_md_check 15 4 = true

Tau.BookIII.Arithmetic.functoriality_15_4

source theorem Tau.BookIII.Arithmetic.functoriality_15_4 :functoriality_check 15 4 = true

Tau.BookIII.Arithmetic.base_change_15_3

source theorem Tau.BookIII.Arithmetic.base_change_15_3 :base_change_check 15 3 = true

Tau.BookIII.Arithmetic.langlands_level

source theorem Tau.BookIII.Arithmetic.langlands_level :Doors.problem_level Doors.MillenniumProblem.Langlands = Enrichment.EnrLevel.E2

[III.D63] Structural: Langlands is at E₁→E₂ interface.

Tau.BookIII.Arithmetic.langlands_part

source theorem Tau.BookIII.Arithmetic.langlands_part :Doors.problem_part Doors.MillenniumProblem.Langlands = 6

Tau.BookIII.Arithmetic.func_10_1

source theorem Tau.BookIII.Arithmetic.func_10_1 :functoriality_check 10 1 = true

[III.T36] Structural: functoriality at depth 1.

Tau.BookIII.Arithmetic.base_change_10_1

source theorem Tau.BookIII.Arithmetic.base_change_10_1 :base_change_check 10 1 = true

[III.T37] Structural: base change at depth 1.