The small prime in the cage estimate

The geometric cage proof starts at p = 7. The target interface also asks for p = 5; this file handles that one finite field by a transparent ambient cardinality bound, not by applying an inapplicable irreducibility statement.

theorem BGS.Markoff.cageSmallPrime_factPrimeFive : Fact (Nat.Prime 5)

theorem BGS.Markoff.natCard_cageMiddleWitnessPowerRangeSolutions_five_le (axis other : NormalizedCoordinateAxis) (xi eta : ZMod 5) (d : ℕ) : Nat.card (cageMiddleWitnessPowerRangeSolutions 5 axis other xi eta d) ≤ 78125

Every witness-bearing power-range set over ZMod 5 has at most 5^7 elements.

theorem BGS.Markoff.cageWitnessPointEstimate_five (axis other : NormalizedCoordinateAxis) (xi eta : ZMod 5) : IsSplitMaximalTrace 5 xi → IsSplitMaximalTrace 5 eta → ∃ (multiplicity : ℕ), 0 < multiplicity ∧ ∀ (d : ℕ), d ∣ Nat.card (ZMod 5)ˣ → 0 < d → |↑(Nat.card (cageMiddleWitnessPowerRangeSolutions 5 axis other xi eta d)) - ↑multiplicity * 5 / ↑d| ≤ 100000 * √5

A coarse uniform estimate at p=5. Multiplicity one is sufficient for this isolated finite case.