One-sided primitive extraction with witness multiplicities

The cage fiber-product count has an arbitrary finite witness type on the left and a cyclic multiplicative group on the right. This file performs Möbius inversion without erasing the left witness.

noncomputable def BGS.rightTraceRelationPairs {A : Type u_1} {H : Type u_2} {T : Type u_3} [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) : Finset (A × H)

Witness/parameter pairs satisfying a relation.

Equations

• BGS.rightTraceRelationPairs leftTrace rightTrace = {z : A × H | leftTrace z.1 = rightTrace z.2}

noncomputable def BGS.rightTraceExactOrderSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (order : ℕ) : Finset (A × H)

Relation pairs whose right parameter has exact multiplicative order.

Equations

• BGS.rightTraceExactOrderSolutions leftTrace rightTrace order = {z ∈ BGS.rightTraceRelationPairs leftTrace rightTrace | orderOf z.2 = order}

noncomputable def BGS.rightTracePowerKernelSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) : Finset (A × H)

Relation pairs whose right parameter is killed by a specified power.

Equations

• BGS.rightTracePowerKernelSolutions leftTrace rightTrace exponent = {z ∈ BGS.rightTraceRelationPairs leftTrace rightTrace | z.2 ^ exponent = 1}

def BGS.rightPowerTraceRangeSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) : Type (max 0 u_1 u_2)

Relation pairs with the right parameter restricted to a power-map image.

Equations

• BGS.rightPowerTraceRangeSolutions leftTrace rightTrace exponent = { z : A × ↥(powMonoidHom exponent).range // leftTrace z.1 = rightTrace ↑z.2 }

def BGS.rightPowerTraceCoverSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) : Type (max 0 u_1 u_2)

The one-sided power cover before quotienting by the power-map fibers.

Equations

• BGS.rightPowerTraceCoverSolutions leftTrace rightTrace exponent = { z : A × H // leftTrace z.1 = rightTrace (z.2 ^ exponent) }

def BGS.rightPowerTraceCoverEquivSigmaFiber {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) : rightPowerTraceCoverSolutions leftTrace rightTrace exponent ≃ (s : rightPowerTraceRangeSolutions leftTrace rightTrace exponent) × ↑(⇑(powMonoidHom exponent) ⁻¹' {↑(↑s).2})

A one-sided cover point is a range solution together with a point in the corresponding power-map fiber.

Equations

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

theorem BGS.natCard_rightPowerTraceCoverSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) : Nat.card (rightPowerTraceCoverSolutions leftTrace rightTrace exponent) = Nat.card ↥(powMonoidHom exponent).ker * Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace exponent)

Exact one-sided power-cover multiplicity.

theorem BGS.natCard_rightPowerTraceCoverSolutions_of_dvd {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] [IsCyclic H] (leftTrace : A → T) (rightTrace : H → T) (d : ℕ) (hd : d ∣ Nat.card H) : Nat.card (rightPowerTraceCoverSolutions leftTrace rightTrace d) = d * Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace d)

For a divisor exponent in a finite cyclic group, the one-sided cover has exactly d points above every power-range solution.

@[simp]

theorem BGS.mem_rightTraceExactOrderSolutions_iff {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (order : ℕ) (z : A × H) : z ∈ rightTraceExactOrderSolutions leftTrace rightTrace order ↔ leftTrace z.1 = rightTrace z.2 ∧ orderOf z.2 = order

@[simp]

theorem BGS.mem_rightTracePowerKernelSolutions_iff {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (exponent : ℕ) (z : A × H) : z ∈ rightTracePowerKernelSolutions leftTrace rightTrace exponent ↔ leftTrace z.1 = rightTrace z.2 ∧ z.2 ^ exponent = 1

theorem BGS.sum_rightTraceExactOrderSolutions_card_eq_powerKernel_card {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (m : ℕ) (hm : 0 < m) : ∑ order ∈ m.divisors, (rightTraceExactOrderSolutions leftTrace rightTrace order).card = (rightTracePowerKernelSolutions leftTrace rightTrace m).card

Exact-order classes partition the relation pairs killed by one power.

theorem BGS.moebius_sum_rightTracePowerKernel_card_eq_exactOrder_card {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (n : ℕ) (hn : 0 < n) : ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑(rightTracePowerKernelSolutions leftTrace rightTrace x.2).card = ↑(rightTraceExactOrderSolutions leftTrace rightTrace n).card

Möbius inversion recovers the witness-bearing exact-order count.

def BGS.rightPowerTraceRangeSolutionsEquivPowerKernelSolutions {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (rangeExponent kernelExponent : ℕ) (hsubgroup : (powMonoidHom rangeExponent).range = (powMonoidHom kernelExponent).ker) : rightPowerTraceRangeSolutions leftTrace rightTrace rangeExponent ≃ ↥(rightTracePowerKernelSolutions leftTrace rightTrace kernelExponent)

A right power-range witness is a right power-kernel witness when the corresponding subgroups agree.

Equations

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

theorem BGS.natCard_rightPowerTraceRangeSolutions_eq_powerKernel_card {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] (leftTrace : A → T) (rightTrace : H → T) (rangeExponent kernelExponent : ℕ) (hsubgroup : (powMonoidHom rangeExponent).range = (powMonoidHom kernelExponent).ker) : Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace rangeExponent) = (rightTracePowerKernelSolutions leftTrace rightTrace kernelExponent).card

theorem BGS.moebius_sum_rightPowerTraceRange_card_eq_exactOrder_card {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] [IsCyclic H] (leftTrace : A → T) (rightTrace : H → T) : ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑(Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace x.1)) = ↑(rightTraceExactOrderSolutions leftTrace rightTrace (Nat.card H)).card

Published one-sided inclusion--exclusion, retaining every left witness.

theorem BGS.rightTraceExactOrderSolutions_card_error_le_moebiusMain {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] [IsCyclic H] (leftTrace : A → T) (rightTrace : H → T) (mainTerm : ℕ → ℝ) (error : ℝ) (hRange : ∀ (d : ℕ), d ∣ Nat.card H → 0 < d → |↑(Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace d)) - mainTerm d| ≤ error) : |↑(rightTraceExactOrderSolutions leftTrace rightTrace (Nat.card H)).card - ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * mainTerm x.1| ≤ ↑(Nat.card H).divisors.card * error

Pointwise range-count estimates give the divisor-count error envelope for the witness-bearing primitive count.

theorem BGS.rightTraceExactOrderSolutions_nonempty_of_divisorsError_lt_moebiusMain {A : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup H] [Finite A] [Finite H] [IsCyclic H] (leftTrace : A → T) (rightTrace : H → T) (mainTerm : ℕ → ℝ) (error : ℝ) (hRange : ∀ (d : ℕ), d ∣ Nat.card H → 0 < d → |↑(Nat.card (rightPowerTraceRangeSolutions leftTrace rightTrace d)) - mainTerm d| ≤ error) (hpositive : ↑(Nat.card H).divisors.card * error < ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * mainTerm x.1) : (rightTraceExactOrderSolutions leftTrace rightTrace (Nat.card H)).Nonempty

If the Möbius main term dominates the divisor error, a primitive right parameter exists together with a genuine left witness.