structure ProjectionTheory.ProjectiveConfigSpace : Type 1

The abstract data of a projective AD-regular configuration space at every scale $\delta$. Each projective configuration embeds into the AD configuration space with matching ratios, and admits a constant-loss decomposition: there exists $C > 0$ such that for every factorization $\delta = \delta_1 \delta_2$ and every configuration $c$ at scale $\delta$, there are configurations $c_1, c_2$ at scales $\delta_1, \delta_2$ with ratio bound $\mathrm{ratio}(c) \le C \cdot \mathrm{ratio}(c_1) \cdot \mathrm{ratio}(c_2)$.

• Config : ℝ → Type
• ratio (δ : ℝ) : self.Config δ → ℝ
• ratio_nonneg (δ : ℝ) (c : self.Config δ) : 0 ≤ self.ratio δ c
• ratio_bddAbove (δ : ℝ) : BddAbove (Set.range (self.ratio δ))
• config_nonempty (δ : ℝ) : Nonempty (self.Config δ)
• embed (δ : ℝ) : self.Config δ → adConfigSpace.Config δ
• embed_ratio (δ : ℝ) (c : self.Config δ) : self.ratio δ c = adConfigSpace.ratio δ (self.embed δ c)
• decompose : ∃ (C : ℝ), 0 < C ∧ ∀ (δ₁ δ₂ : ℝ), 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → ∀ (c : self.Config (δ₁ * δ₂)), ∃ (c₁ : self.Config δ₁) (c₂ : self.Config δ₂), self.ratio (δ₁ * δ₂) c ≤ C * (self.ratio δ₁ c₁ * self.ratio δ₂ c₂)

structure ProjectionTheory.ProjectiveConfigData : Type 1

The raw data underlying a projective AD configuration space: configurations with explicit coarsen/restrict maps, and the pointwise incidence decomposition bound with a universal constant $C$.

• Config : ℝ → Type
• ratio (δ : ℝ) : self.Config δ → ℝ
• ratio_nonneg (δ : ℝ) (c : self.Config δ) : 0 ≤ self.ratio δ c
• ratio_bddAbove (δ : ℝ) : BddAbove (Set.range (self.ratio δ))
• config_nonempty (δ : ℝ) : Nonempty (self.Config δ)
• embed (δ : ℝ) : self.Config δ → adConfigSpace.Config δ
• embed_ratio (δ : ℝ) (c : self.Config δ) : self.ratio δ c = adConfigSpace.ratio δ (self.embed δ c)
• coarsen (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₁
• restrict (δ₁ δ₂ : ℝ) : 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → self.Config (δ₁ * δ₂) → self.Config δ₂
• incidence_decomp : ∃ (C : ℝ), 0 < C ∧ ∀ (δ₁ δ₂ : ℝ) (hδ₁ : 0 < δ₁) (hδ₁' : δ₁ < 1) (hδ₂ : 0 < δ₂) (hδ₂' : δ₂ < 1) (c : self.Config (δ₁ * δ₂)), self.ratio (δ₁ * δ₂) c ≤ C * (self.ratio δ₁ (self.coarsen δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c) * self.ratio δ₂ (self.restrict δ₁ δ₂ hδ₁ hδ₁' hδ₂ hδ₂' c))

noncomputable def ProjectionTheory.projConfigData : ProjectiveConfigData

The concrete projective AD configuration data used in the projection theory framework.

noncomputable def ProjectionTheory.projConfigSpace : ProjectiveConfigSpace

The projective AD configuration space obtained from projConfigData by extracting the pointwise incidence decomposition into a decomposition existence statement.

noncomputable def ProjectionTheory.R_AD_proj (δ : ℝ) : ℝ

The projective AD-regular incidence quantity $R_{AD,\mathrm{proj}}(\delta)$ at scale $\delta$, defined as the supremum of the projective configuration ratios at scale $\delta$.

theorem ProjectionTheory.proj_ratio_le_R_AD_proj (δ : ℝ) (c : projConfigSpace.Config δ) : projConfigSpace.ratio δ c ≤ R_AD_proj δ

Each projective configuration ratio is bounded above by the supremum $R_{AD,\mathrm{proj}}(\delta)$.

theorem ProjectionTheory.R_AD_proj_nonneg (δ : ℝ) : 0 ≤ R_AD_proj δ

$R_{AD,\mathrm{proj}}(\delta) \ge 0$ for every scale $\delta$.

theorem ProjectionTheory.R_AD_proj_submultiplicative : ∃ (C : ℝ), 0 < C ∧ ∀ (δ₁ δ₂ : ℝ), 0 < δ₁ → δ₁ < 1 → 0 < δ₂ → δ₂ < 1 → R_AD_proj (δ₁ * δ₂) ≤ C * R_AD_proj δ₁ * R_AD_proj δ₂

Submultiplicative Lemma, projective version. There exists a constant $C > 0$ such that whenever $\delta = \delta_1 \delta_2$ with $\delta_1, \delta_2 < 1$, $R_{AD,\mathrm{proj}}(\delta_1 \delta_2) \le C \cdot R_{AD,\mathrm{proj}}(\delta_1) \cdot R_{AD,\mathrm{proj}}(\delta_2)$.