From slope form to the original coefficient form

The bookkeeping step from the normalized slope count to the coefficient statement of the original conjecture: dividing the coefficient equation v₁ x + v₂ y + (v₁+v₂) z = 0 through by v₁ turns it into the normalized equation at slope ρ = v₂/v₁.

coefficientTripleCount itself is the audited definition from KasamiCyclicAdditive.Statement.Definitions.

Assembly/CoefficientReduction.lean and Assembly/Normalization.lean import this module; coefficient_form_nat_of_slope_form is what carries the assembled slope theorem back to the coefficient form of the original conjecture.

theorem KasamiCyclicAdditive.coefficientTripleCount_eq_slopeTripleCount {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {k : ℕ} {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) : coefficientTripleCount k v₁ v₂ = slopeTripleCount k (v₂ / v₁)

Dividing the coefficient equation by v₁ gives the normalized slope ρ=v₂/v₁. No characteristic-two hypothesis is needed for this bookkeeping identity.

theorem KasamiCyclicAdditive.coefficientSlope_admissible {K : Type u_1} [Field K] {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : AdmissibleSlope (v₂ / v₁)

Distinct nonzero coefficients give an admissible normalized slope.

theorem KasamiCyclicAdditive.coefficient_form_of_slope_form {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {k : ℕ} {c : ℝ} (hslope : ∀ ρ ∈ slopes K, ↑(slopeTripleCount k ρ) = c) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : ↑(coefficientTripleCount k v₁ v₂) = c

Any theorem proved uniformly for all admissible slopes immediately yields the original coefficient-form theorem.

theorem KasamiCyclicAdditive.card_sq_div_eight_eq_pow {K : Type u_1} [Fintype K] {n : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) : ↑(Fintype.card K) ^ 2 / 8 = ↑(2 ^ (2 * n - 3))

The real-valued main term |K|^2/8 is the natural number 2^(2n-3) when |K| = 2^n and n ≥ 2.

theorem KasamiCyclicAdditive.coefficient_form_nat_of_slope_form {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {n k : ℕ} (hn : 2 ≤ n) (hcard : Fintype.card K = 2 ^ n) (hslope : ∀ ρ ∈ slopes K, ↑(slopeTripleCount k ρ) = ↑(Fintype.card K) ^ 2 / 8) {v₁ v₂ : K} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) (hne : v₁ ≠ v₂) : coefficientTripleCount k v₁ v₂ = 2 ^ (2 * n - 3)

Natural-number version of the original coefficient statement, obtained from a slope theorem with the standard real main term.