The weighted-trace torsion-intersection bound

This module records the exact numerical statement consumed by the Markoff middle game. The statement is intentionally independent of how the estimate is proved, so low-level escape lemmas do not import the full general Corvaja--Zannier development.

The bound is uniform in the two weights and the two torsion orders. Its hypotheses expose the actual curve admissibility, positivity, and prime-to-characteristic requirements. The completed producer corvajaZannierWeightedTraceBound supplies this statement from the in-repository general Corvaja--Zannier theorem.

The conclusion is the safe coefficient-48 envelope used by the downstream middle game. This permits the genuine degree-only Euler bound χ ≤ 8 for a general bidegree-(2,2) torus curve; no unsupported genus-one identification is built into the interface.

def BGS.Markoff.WeightedTraceTorsionIntersectionBound (p : ℕ) (E : Type u_1) [Field E] [Fintype E] : Prop

The numerical weighted-trace torsion-intersection statement used by the middle game.

This is a lightweight internal proof boundary, not an external assumption. The selected BGS path constructs it with corvajaZannierWeightedTraceBound.

Equations

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

theorem BGS.Markoff.multiplicativeSubgroups_satisfy_weightedTraceBoundOrderHypotheses (p : ℕ) [Fact (Nat.Prime p)] (E : Type u_1) [Field E] [CharP E p] [Finite E] (H₁ H₂ : Subgroup Eˣ) : 0 < Nat.card ↥H₁ ∧ 0 < Nat.card ↥H₂ ∧ ¬p ∣ Nat.card ↥H₁ ∧ ¬p ∣ Nat.card ↥H₂

Multiplicative subgroup orders satisfy every arithmetic side condition in the weighted-trace torsion-intersection bound.

theorem BGS.Markoff.weightedTraceEquationSolutions_card_cast_le_of_weightedTraceBound (p : ℕ) [Fact (Nat.Prime p)] (E : Type u_1) [Field E] [Fintype E] [CharP E p] (hBound : WeightedTraceTorsionIntersectionBound p E) (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) (hadmissible : WeightedTraceCurveIsCorvajaZannierAdmissible alpha beta) : ↑(weightedTraceEquationSolutions alpha beta H₁ H₂).card ≤ corvajaZannierTraceUpperBound p (Nat.card ↥H₁) (Nat.card ↥H₂)

Apply the weighted-trace torsion-intersection bound after Lean has proved the concrete curve is admissible and both subgroup orders satisfy the source's arithmetic hypotheses.