WIP: import Markoff mod p - #502

Open

Vilin97 wants to merge 51 commits into

mainfrom

codex/import42-markoff-modp

Commits on Sep 21, 2026

Import Markoff mod p
Vilin97
committed
50bc00d
Refine full import for Lean 4.34 compatibility and quality checks
Vilin97
committed
93d687f
Port algebraic frontiers and share the separable relative norm theorem
Vilin97
committed
29ee4a7
Repair normalized coordinates and function-field dependency APIs
Vilin97
committed
6a765b6
Port divisor, curve and gluing proofs to current Mathlib
Vilin97
committed
6fbe258
Port Markoff divisor, weighted counting, and formal zeta dependencies
Vilin97
committed
9f41cce
Port remaining finite-place dependencies and reduce torsion proof elaboration
Vilin97
committed
83187f7
Port affine places, infinity localizations, and canonical degree bounds
Vilin97
committed
eeed404
Port constant fields and trace-curve normalization proofs
Vilin97
committed
0b0a3ed
Factor boundary degree transport through generic valuation models
Vilin97
committed
0faff57
Port function field place and constant field instances
Vilin97
committed
7c183e4

Commits on Sep 22, 2026

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot]
committed
4de9dc4

Commits on Sep 25, 2026

Commits on Sep 26, 2026