Skip to content

WIP: import Markoff mod p #502

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 51 commits into
base: main
Choose a base branch
from
Open

WIP: import Markoff mod p #502

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
50bc00d
Import Markoff mod p
Vilin97 Sep 21, 2026
93d687f
Refine full import for Lean 4.34 compatibility and quality checks
Vilin97 Sep 21, 2026
29ee4a7
Port algebraic frontiers and share the separable relative norm theorem
Vilin97 Sep 21, 2026
6a765b6
Repair normalized coordinates and function-field dependency APIs
Vilin97 Sep 21, 2026
6fbe258
Port divisor, curve and gluing proofs to current Mathlib
Vilin97 Sep 21, 2026
9f41cce
Port Markoff divisor, weighted counting, and formal zeta dependencies
Vilin97 Sep 21, 2026
83187f7
Port remaining finite-place dependencies and reduce torsion proof ela…
Vilin97 Sep 21, 2026
eeed404
Port affine places, infinity localizations, and canonical degree bounds
Vilin97 Sep 21, 2026
0b0a3ed
Port constant fields and trace-curve normalization proofs
Vilin97 Sep 21, 2026
0faff57
Factor boundary degree transport through generic valuation models
Vilin97 Sep 21, 2026
7c183e4
Port function field place and constant field instances
Vilin97 Sep 21, 2026
1b28927
Factor Riemann dimension and exceptional-place arguments
Vilin97 Sep 22, 2026
5a071bf
Factor exact constant extension different comparison
Vilin97 Sep 22, 2026
882977b
Factor valuation-center and residue-degree comparisons
Vilin97 Sep 22, 2026
928d77a
Repair constant extension regularity and weighted trace bounds
Vilin97 Sep 22, 2026
1331ed5
Factor smooth residue normalization and constant-base algebra arguments
Vilin97 Sep 22, 2026
fe64c14
Factor infinity different through generic field-range base change
Vilin97 Sep 22, 2026
c093bb7
Repair Frobenius-twist descent and intermediate field finiteness
Vilin97 Sep 22, 2026
e1ffee8
Factor local different nonvanishing and normalization injectivity
Vilin97 Sep 22, 2026
aaa1157
Separate canonical constant-compositum comparisons
Vilin97 Sep 22, 2026
6244dd9
Factor affine residue centers through general valuation lemmas
Vilin97 Sep 22, 2026
cd7fd10
Update finite-place averages to scalar towers and field dimensions
Vilin97 Sep 22, 2026
c0d2c12
Port Markoff warning spellings, explicit imports and kernel certificates
Vilin97 Sep 22, 2026
8d28b4e
Declare downstream geometric and spectral imports explicitly
Vilin97 Sep 22, 2026
35ab821
Port Markoff ramification and split local dimension proofs
Vilin97 Sep 22, 2026
d78b54a
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 22, 2026
f6b8dc6
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 23, 2026
e7b9b02
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 23, 2026
4de9dc4
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 24, 2026
f5e9723
Repair Markoff normal-closure counts and refactor place averaging
Vilin97 Sep 25, 2026
7a51d36
Migrate Markoff modules and factor constant-extension proofs
Vilin97 Sep 25, 2026
eeaaeca
docs(MarkoffModP): clarify monogenicity source and supporting authorship
Vilin97 Sep 25, 2026
e3a9026
Merge current main while preserving all project cards
Vilin97 Sep 25, 2026
daf0251
Repair Markoff module interfaces and remove unused assumptions
Vilin97 Sep 25, 2026
a664a9f
Merge remote-tracking branch 'origin/codex/import42-markoff-modp' int…
Vilin97 Sep 25, 2026
3640b4b
Restore generated Markoff imports and generalize finite counting assu…
Vilin97 Sep 25, 2026
9c5c9d9
Generalize Markoff finite counting lemmas and clean compiler warnings
Vilin97 Sep 25, 2026
eff45ff
Factor the Hasse-Weil tower estimate and simplify proof assumptions
Vilin97 Sep 25, 2026
c1c17cc
Expose required Markoff interfaces and remove redundant section assum…
Vilin97 Sep 26, 2026
07d26f2
Merge remote-tracking branch 'origin/main' into codex/import42-markof…
Vilin97 Sep 26, 2026
d1b7566
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
795228f
Share exported Markoff field proofs and trim unused section hypotheses
Vilin97 Sep 26, 2026
3dac82b
Merge remote-tracking branch 'origin/codex/import42-markoff-modp' int…
Vilin97 Sep 26, 2026
7e79885
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 26, 2026
1aecff2
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 26, 2026
5ebcced
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 26, 2026
8823542
Fix Markoff support bounds and public normalization hypotheses
Vilin97 Sep 26, 2026
51fb19a
Expand private Markoff point aliases in public hypotheses
Vilin97 Sep 26, 2026
ca3684d
Expand joint normalization alias in public frontier statements
Vilin97 Sep 26, 2026
6a6db8a
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 26, 2026
9e580aa
Merge remote-tracking branch 'origin/main' into pr-502
github-actions[bot] Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
610 changes: 610 additions & 0 deletions LeanPool.lean
View file
Open in desktop

Large diffs are not rendered by default.

628 changes: 628 additions & 0 deletions LeanPool/MarkoffModP.lean
View file
Open in desktop

Large diffs are not rendered by default.

159 changes: 159 additions & 0 deletions LeanPool/MarkoffModP/BGS.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,159 @@
/-
Copyright (c) 2026 Yuma Mizuno. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yuma Mizuno
-/
module


public import LeanPool.MarkoffModP.BGS.NumberTheory.DivisorBound
public import LeanPool.MarkoffModP.BGS.NumberTheory.OneSidedPrimitiveWitness
public import LeanPool.MarkoffModP.BGS.Algebra.KummerEigencharacterDescent
public import LeanPool.MarkoffModP.BGS.Algebra.DifferentialWronskian
public import LeanPool.MarkoffModP.BGS.Algebra.RatFuncLinearFractionalEquiv
public import LeanPool.MarkoffModP.BGS.Algebra.ClearedLinearFractionalSubstitution
public import LeanPool.MarkoffModP.BGS.FiniteField.HasseFrobenius
public import LeanPool.MarkoffModP.BGS.Dynamics.StrictMeasureEscape
public import LeanPool.MarkoffModP.BGS.External.GeneralCurveTheorems
public import LeanPool.MarkoffModP.RiemannRoch.CoordinateFree.AlgEquiv
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneSquareFieldStepanovCountAutomatic
public import LeanPool.MarkoffModP.BGS.HasseWeil.GeneralSquareFieldStepanovCount
public import LeanPool.MarkoffModP.BGS.HasseWeil.RatFuncParameterPole
public import LeanPool.MarkoffModP.BGS.HasseWeil.GeneralFiniteExtensionRiemannLower
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannLowerFromGenus
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannEventualGrowth
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannShiftedEventualGrowth
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannSpaceProjectivization
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionPlaceDegreeFiniteness
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionAffineIdealDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionAffineIdealDivisor
public import LeanPool.MarkoffModP.BGS.HasseWeil.GeneralSquareFieldStepanovCountAutomatic
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExtensionEvenDegreeStepanovBound
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneCoordinateShear
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneFrobeniusDeflation
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneFrobeniusDegenerate
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneFrobeniusReduction
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaHasseBound
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaRationality
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaRationalityDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaUniqueness
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaEuler
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaEulerDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaDegreeIndexOne
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaDegreeIndexOneIndexed
public import LeanPool.MarkoffModP.BGS.HasseWeil.FormalZetaConstantExtensionIdentity
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeExtensionIdentity
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionDivisorDegreeIndex
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionEffectiveDivisorSplit
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionDivisorClassRecurrence
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionRiemannRoch
public import LeanPool.MarkoffModP.BGS.HasseWeil.RatFuncCanonicalInfinityDivisor
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCanonicalDifferentGenusBound
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCanonicalDifferentCanonicalityCriterion
public import LeanPool.MarkoffModP.BGS.HasseWeil.DedekindDifferentLocalTrace
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCanonicalDifferentCotrace
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCotraceLocalTraceImage
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCanonicalDifferentCotraceCanonicality
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionCanonicalDifferentLocalMaximality
public import LeanPool.MarkoffModP.BGS.HasseWeil.LinearFunctionalGluing
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionGenusBound
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneCurveGenusBoundFromCotraceDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneCurveGenusBoundFromCotrace
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneCurveGenusBoundAutomatic
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineFiberBound
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineRationalPlaceComparison
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneRationalPlaceAffineComparison
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineCountTransfer
public import LeanPool.MarkoffModP.BGS.HasseWeil.ClosedPlaceEulerRecurrence
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionIndexedZetaRationality
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionIndexedZetaRationalityAutomatic
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaSimplePole
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaNumeratorNoncancellation
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeIndexOne
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeIndexOneFromAllCounts
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionZetaDegreeIndexOneAutomatic
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionStandardZetaRationality
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionClosedPlaceCount
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionPlaceSplittingMultiplicity
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionInfinityPlaceDegreeTower
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionClosedPlaceSplittingFormula
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionPlaceTower
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteBranchLocus
public import LeanPool.MarkoffModP.BGS.HasseWeil.RationalPlace
public import LeanPool.MarkoffModP.BGS.HasseWeil.RationalPlaceTower
public import LeanPool.MarkoffModP.BGS.HasseWeil.RatFuncConstantExtension
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldConstantExtension
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldAutomorphism
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldRatFuncCompatibility
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldFinitePlace
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldFinitePlaceDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantFieldInfinityBase
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosure
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldConstantField
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureConstants
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtension
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionAutomorphism
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionConstants
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionQuotient
public import LeanPool.MarkoffModP.BGS.HasseWeil.FrobeniusTwistGroup
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwist
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistConstants
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistRiemannLower
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistMultiplication
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureConstantBase
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureRatFuncBase
public import LeanPool.MarkoffModP.BGS.HasseWeil.FunctionFieldNormalClosureRatFuncEquiv
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldSubfield
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldCompositum
public import LeanPool.MarkoffModP.BGS.HasseWeil.PolynomialTensorCancel
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldPolynomialNormalization
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldPolynomialDifferent
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldInfinityDifferent
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionInfinityDifferent
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFiniteDifferent
public import LeanPool.MarkoffModP.BGS.HasseWeil.FinsuppWeightedFiber
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionTotalDifferentEffectiveDivisor
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionTotalDifferentDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionGenusInvariance
public import LeanPool.MarkoffModP.BGS.HasseWeil.IdealMultiplicityMap
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionGenusDegree
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldConstantExtensionNormalization
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantTensorResidue
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteFieldConstantExtensionResidue
public import LeanPool.MarkoffModP.BGS.HasseWeil.FinitePlaceNormalizationTransport
public import LeanPool.MarkoffModP.BGS.HasseWeil.RatFuncExactConstantExtension
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionFinitePlaceBridge
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionRationalPlace
public import LeanPool.MarkoffModP.BGS.HasseWeil.RatFuncInfinityLocalization
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionInfinityNormalization
public import LeanPool.MarkoffModP.BGS.HasseWeil.ConstantExtensionInfinityPlaceBridge
public import LeanPool.MarkoffModP.BGS.HasseWeil.FinitePlaceFrobeniusFiber
public import LeanPool.MarkoffModP.BGS.HasseWeil.FrobeniusPlaceCardinality
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFinitePlace
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFinitePlaceCompatibility
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFinitePlaceFrobeniusAverage
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistFinitePlaceAverage
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistRationalPlaceAverage
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistFinitePlaceBridge
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistFinitePlaceUnramified
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistInfinityPlaceDescent
public import LeanPool.MarkoffModP.BGS.HasseWeil.ExactConstantExtensionFrobeniusTwistInfinityPlaceEquivalence
public import LeanPool.MarkoffModP.BGS.HasseWeil.FiniteExtensionHasseBoundFromEvenConstantExtensions
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineHasseWeilFromZeta
public import LeanPool.MarkoffModP.BGS.HasseWeil.PlaneAffineHasseWeilFromEvenError
public import LeanPool.MarkoffModP.BGS.HasseWeil.GeneralBivariateAffineHasseWeil
public import LeanPool.MarkoffModP.BGS.CorvajaZannier
public import LeanPool.MarkoffModP.BGS.Markoff.Core
public import LeanPool.MarkoffModP.BGS.Markoff.Opening
public import LeanPool.MarkoffModP.BGS.Markoff.MiddleGame
public import LeanPool.MarkoffModP.BGS.Markoff.TraceCurve
public import LeanPool.MarkoffModP.BGS.Markoff.Endgame
public import LeanPool.MarkoffModP.BGS.Markoff.Cage
public import LeanPool.MarkoffModP.BGS.Markoff.Incidence
public import LeanPool.MarkoffModP.BGS.Markoff.Assembly
public import LeanPool.MarkoffModP.BGS.Markoff.Diophantine
public import LeanPool.MarkoffModP.BGS.Markoff.Assembly.RankinWidthEnvelope
public import LeanPool.MarkoffModP.BGS.Markoff.Assembly.RankinJointAntichainWidth
public import LeanPool.MarkoffModP.BGS.Markoff.Assembly.RankinJointAntichainSperner
public import LeanPool.MarkoffModP.BGS.NumberTheory.RankinCutoff1248Profile
Loading
Loading