NYLL
Module

Theorem2Dot4DyadicCollision.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Theorem2Dot4DyadicCollision
5 declarations indexed from sourceView source ↗

Module documentation

Lemma 2.4: three sections meeting in the dyadic special fibre

The finite-boundary declaration is exists_two_le_padicValInt_delta_in_boundary.

The support of a rational section is the actual homogeneous zero locus of v*T₀-u*T₁ in ℙ¹_ℤ, using primitive integral coordinates of the rational projective point. Membership after the coefficient morphism from ℙ¹_𝔽₂ is reduced to membership of this equation modulo two in the point's homogeneous prime ideal.

The irrelevant-ideal condition excludes simultaneous vanishing of both coordinates. The common point therefore forces all three primitive pairs to have the same one of the three parity types. The identity, subtraction, or interchange of coordinates reduces to the previously proved dyadic pigeonhole calculation. Distinct rational points have nonzero determinant, so divisibility by four yields the original bound on the dyadic valuation. No unproved intersection-multiplicity or coordinate-normalization assertion is taken as input.

Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Lemma 2.4. The proof works for every point in the special fibre; the original closed-point hypothesis is unnecessary.

Imports21
Imported by1

Declarations

theorem

primitive_not_both_even

L63 ↗
ShimizuYamaguchi26BranchedCoverings.primitive_not_both_even
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem primitive_not_both_even (u v : ℤ) (hprimitive : IsCoprime u v)
    (hu : Even u) (hv : Even v) : False
theorem

primitive_section_parity

L72 ↗
ShimizuYamaguchi26BranchedCoverings.primitive_section_parity
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem primitive_section_parity (x : ProjectiveLine (ZMod 2))
    (u v : ℤ) (hprimitive : IsCoprime u v)
    (hsection : linearSectionEquation (u : ZMod 2) (v : ZMod 2) ∈ x.asHomogeneousIdeal) :
    (Even u ∧ Odd v ∧ MvPolynomial.X (0 : Fin 2) ∈ x.asHomogeneousIdeal) ∨
      (Odd u ∧ Even v ∧ MvPolynomial.X (1 : Fin 2) ∈ x.asHomogeneousIdeal) ∨
      (Odd u ∧ Odd v ∧
        MvPolynomial.X (0 : Fin 2) - MvPolynomial.X (1 : Fin 2) ∈ x.asHomogeneousIdeal)
theorem

exists_four_dvd_coordinateDeterminant_of_common_specialFiber_point

L98 ↗
ShimizuYamaguchi26BranchedCoverings.exists_four_dvd_coordinateDeterminant_of_common_specialFiber_point
Documentation

Three primitive integral section equations through an actual point of ℙ¹_𝔽₂ have a pair of determinants divisible by four. All parity normalization is derived from that common point.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem exists_four_dvd_coordinateDeterminant_of_common_specialFiber_point
    (u v : Fin 3 → ℤ) (hprimitive : ∀ i : Fin 3, IsCoprime (u i) (v i))
    (x : ProjectiveLine (ZMod 2))
    (hsection : ∀ i : Fin 3,
      linearSectionEquation (u i : ZMod 2) (v i : ZMod 2) ∈ x.asHomogeneousIdeal) :
    ∃ i j : Fin 3, i ≠ j ∧ (4 : ℤ) ∣ coordinateDeterminant (u i) (v i) (u j) (v j)
theorem

exists_two_le_padicValInt_delta_of_three_sections

L157 ↗
ShimizuYamaguchi26BranchedCoverings.exists_two_le_padicValInt_delta_of_three_sections
Documentation

Lemma 2.4 for three distinct rational projective points: their integral section supports meeting in the dyadic special fibre forces the original intersection determinant to have dyadic valuation at least two.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem exists_two_le_padicValInt_delta_of_three_sections
    (a : Fin 3 → Projectivization ℚ (ℚ × ℚ)) (ha : Function.Injective a)
    (x : ProjectiveLine (ZMod 2))
    (hsection : ∀ i : Fin 3, (ProjSpace.map ℤ (ZMod 2) 1) x ∈ rationalSectionSupport (a i)) :
    ∃ i j : Fin 3, i ≠ j ∧ 2 ≤ padicValInt 2 (rationalPointDelta (a i) (a j))
theorem

exists_two_le_padicValInt_delta_in_boundary

L183 ↗
ShimizuYamaguchi26BranchedCoverings.exists_two_le_padicValInt_delta_in_boundary
Documentation

The finite-boundary formulation of Lemma 2.4, with the two distinct witnesses retained in the original set of rational points.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem exists_two_le_padicValInt_delta_in_boundary
    (A : Finset (Projectivization ℚ (ℚ × ℚ)))
    (a : Fin 3 → Projectivization ℚ (ℚ × ℚ)) (ha : Function.Injective a)
    (hA : ∀ i : Fin 3, a i ∈ A) (x : ProjectiveLine (ZMod 2))
    (hsection : ∀ i : Fin 3, (ProjSpace.map ℤ (ZMod 2) 1) x ∈ rationalSectionSupport (a i)) :
    ∃ b ∈ A, ∃ c ∈ A, b ≠ c ∧ 2 ≤ padicValInt 2 (rationalPointDelta b c)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.