Iteration of the prime-refinement lemma

The model-independent separator theorem drives one recursive construction over prime factors. It flattens the resulting nested power partitions and derives the arbitrary-number fair-partition theorem. The fixed Fox--Neuwirth interface specializes that same construction.

@[reducible, inline]

abbrev NRR.PrimeFactor : Type

A natural number equipped with a proof of primality.

Equations

• NRR.PrimeFactor = { p : ℕ // Nat.Prime p }

def NRR.primeFactorProduct (ps : List PrimeFactor) : ℕ

Product of a list of prime factors.

Equations

• NRR.primeFactorProduct ps = (List.map Subtype.val ps).prod

def NRR.PrimeRefinementIndex : List PrimeFactor → Type

The nested finite index type generated by successive prime refinements.

Equations

• NRR.PrimeRefinementIndex [] = Unit
• NRR.PrimeRefinementIndex (p :: ps) = (Fin ↑p × NRR.PrimeRefinementIndex ps)

@[instance_reducible]

noncomputable instance NRR.primeRefinementIndexFintype (ps : List PrimeFactor) : Fintype (PrimeRefinementIndex ps)

Equations

• NRR.primeRefinementIndexFintype [] = inferInstance
• NRR.primeRefinementIndexFintype (p :: ps) = inferInstance

@[simp]

theorem NRR.card_primeRefinementIndex (ps : List PrimeFactor) : Fintype.card (PrimeRefinementIndex ps) = primeFactorProduct ps

noncomputable def NRR.primeDescendArea (A : ℝ) : List PrimeFactor → ℝ

Repeatedly divide an area threshold by the listed primes.

Equations

• NRR.primeDescendArea A [] = A
• NRR.primeDescendArea A (p :: ps) = NRR.primeDescendArea (A / ↑↑p) ps

theorem NRR.primeDescendArea_pos {A : ℝ} (hA : 0 < A) (ps : List PrimeFactor) : 0 < primeDescendArea A ps

Repeated prime descent preserves positivity.

def NRR.bundledPrimeFactors (n : ℕ) : List PrimeFactor

The prime factors of a positive natural number, bundled with primality proofs.

Equations

• NRR.bundledPrimeFactors n = List.map (fun (p : { x : ℕ // x ∈ n.primeFactorsList }) => ⟨↑p, ⋯⟩) n.primeFactorsList.attach

@[simp]

theorem NRR.primeFactorProduct_bundledPrimeFactors {n : ℕ} (hn : n ≠ 0) : primeFactorProduct (bundledPrimeFactors n) = n

structure NRR.IteratedPartitionWitness {K : Geometry.ConvexBody Geometry.Plane} (ps : List PrimeFactor) (A : ℝ) (hA : 0 < A) (φ : NiceMV (BodySpace K (primeDescendArea A ps))) (C : BodySpace K A) (y : ↑SignedInterval) : Type

The flattened partition data decoded from an iterated refined zero.

• partition : IndexedConvexPartition (EMP.VariableBody.solidBody hA C) (PrimeRefinementIndex ps)

  The indexed convex partition decoded from the iterated refinement.

• leaf : PrimeRefinementIndex ps → BodySpace K (primeDescendArea A ps)

  The leaf body associated with each sequence of prime-refinement choices.

• piece_eq_leaf (i : PrimeRefinementIndex ps) : (self.partition.piece i).carrier = ↑(self.leaf i).body.body
• piece_area_eq (i : PrimeRefinementIndex ps) : Geometry.ConvexBody.area (self.partition.piece i) = primeDescendArea C.body.area ps
• leaf_zero (i : PrimeRefinementIndex ps) : φ.Zero (self.leaf i) y

structure NRR.IteratedRefinement {K : Geometry.ConvexBody Geometry.Plane} (ps : List PrimeFactor) (A : ℝ) (hA : 0 < A) (φ : NiceMV (BodySpace K (primeDescendArea A ps))) : Type

A nice multivalued function obtained by iterating prime refinement, together with the decoder from each output zero to the flattened partition witness.

• output : NiceMV (BodySpace K A)

  The multivalued observable on the parent body produced by all prime-refinement steps.

• decode (C : BodySpace K A) (y : ↑SignedInterval) : self.output.Zero C y → IteratedPartitionWitness ps A hA φ C y

  Decode a zero of the parent observable into a partition witness with zero-valued leaves.

noncomputable def NRR.FlexibleIteratedRefinement.build {K : Geometry.ConvexBody Geometry.Plane} (H : FlexiblePrimeRefinementTheorem) (ps : List PrimeFactor) (A : ℝ) (hA : 0 < A) (hAK : A ≤ K.area) (φ : NiceMV (BodySpace K (primeDescendArea A ps))) : IteratedRefinement ps A hA φ

Build the full iterated refinement from the model-independent separator theorem.

Equations

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

noncomputable def NRR.IteratedRefinement.build {K : Geometry.ConvexBody Geometry.Plane} (H : PrimeRefinementTheorem) (ps : List PrimeFactor) (A : ℝ) (hA : 0 < A) (hAK : A ≤ K.area) (φ : NiceMV (BodySpace K (primeDescendArea A ps))) : IteratedRefinement ps A hA φ

Specialize the shared model-independent iteration to the fixed Fox--Neuwirth model.

Equations

• NRR.IteratedRefinement.build H ps A hA hAK φ = NRR.FlexibleIteratedRefinement.build ⋯ ps A hA hAK φ

theorem NRR.IteratedPartitionWitness.partition_isEqualArea {K : Geometry.ConvexBody Geometry.Plane} {ps : List PrimeFactor} {A : ℝ} {hA : 0 < A} {φ : NiceMV (BodySpace K (primeDescendArea A ps))} {C : BodySpace K A} {y : ↑SignedInterval} (W : IteratedPartitionWitness ps A hA φ C y) : W.partition.IsEqualArea

The decoded flattened partition has equal area.

theorem NRR.IteratedPartitionWitness.partition_hasEqualPerimeter {K : Geometry.ConvexBody Geometry.Plane} {ps : List PrimeFactor} {A : ℝ} {hA : 0 < A} {C : BodySpace K A} {y : ↑SignedInterval} (W : IteratedPartitionWitness ps A hA (perimeterNiceMV K (primeDescendArea A ps) ⋯) C y) : W.partition.HasEqualPerimeter

When the leaf function is the normalized perimeter observable, all flattened pieces have equal perimeter because every leaf is a zero at the same signed parameter.

theorem NRR.exists_fair_partition_of_flexiblePrimeRefinement (H : FlexiblePrimeRefinementTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) (hn : 0 < n) : ∃ (P : ConvexPartition K n), P.IsFair

Arbitrary-number AAK theorem from the model-independent separator theorem.

theorem NRR.exists_fair_partition_of_primeRefinement (H : PrimeRefinementTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) (hn : 0 < n) : ∃ (P : ConvexPartition K n), P.IsFair

Arbitrary-number AAK theorem from the prime-refinement separator theorem.

theorem NRR.avvakumov_akopyan_karasev_of_primeRefinement (H : PrimeRefinementTheorem) (K : Geometry.ConvexBody Geometry.Plane) (n : ℕ) : 0 < n → ∃ (P : ConvexPartition K n), P.IsFair

Public implication form of the Avvakumov--Akopyan--Karasev theorem. The conclusion for every positive number of pieces follows formally from the single prime-refinement separator theorem.