Cartesian powers for approximate counting

The row-major encoding preserves both membership and the exact power-law cardinality required by Stockmeyer's accuracy amplification.

theorem Complexity.ApproximateCounting.mem_cartesianPower_iff {domainWidth copies : ℕ} {set : Finset (BitString domainWidth)} {input : BitString (copies * domainWidth)} : input ∈ cartesianPower set copies ↔ ∀ (copy : Fin copies), (blocksEquiv copies domainWidth) input copy ∈ set

A packed string belongs to the Cartesian power exactly when every decoded block belongs to the original set.

theorem Complexity.ApproximateCounting.card_cartesianPower {domainWidth : ℕ} (set : Finset (BitString domainWidth)) (copies : ℕ) : (cartesianPower set copies).card = set.card ^ copies

The copies-fold Cartesian power has cardinality |set| ^ copies.

theorem Complexity.ApproximateCounting.relativeCopies_separates_sixteen (precision : ℕ) (hprecision : 0 < precision) : 16 ^ 2 * precision ^ relativeCopies precision ≤ (precision + 1) ^ relativeCopies precision

Eight copies per precision unit separate the two endpoints of a factor-16 uncertainty interval after taking roots.

theorem Complexity.ApproximateCounting.upperRootEstimate_isRelativeApproximation {factor copies precision actual weakEstimate : ℕ} (hcopies : 0 < copies) (hprecision : 0 < precision) (hseparation : factor ^ 2 * precision ^ copies ≤ (precision + 1) ^ copies) (hweak : IsFactorApproximation factor (actual ^ copies) weakEstimate) : IsRelativeApproximation precision actual (upperRootEstimate factor copies weakEstimate)

Scaling a factor estimate by that factor before taking a floor root gives a relative estimate whenever the chosen power separates the endpoints.

theorem Complexity.ApproximateCounting.boostedEstimate_isRelativeApproximation {precision actual weakEstimate : ℕ} (hprecision : 0 < precision) (hweak : IsFactorApproximation 16 (actual ^ relativeCopies precision) weakEstimate) : IsRelativeApproximation precision actual (boostedEstimate precision weakEstimate)

A factor-16 estimate of the prescribed power yields relative error at most 1 / precision, including exact preservation of zero.

theorem Complexity.ApproximateCounting.boostedEstimate_cartesianPower_isRelativeApproximation {domainWidth precision weakEstimate : ℕ} (set : Finset (BitString domainWidth)) (hprecision : 0 < precision) (hweak : IsFactorApproximation 16 (cartesianPower set (relativeCopies precision)).card weakEstimate) : IsRelativeApproximation precision set.card (boostedEstimate precision weakEstimate)

Applying the factor-to-relative conversion to a Cartesian power recovers a relative estimate of the original set cardinality.