mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
1a26de076d
- ChentsovFinite.lean: Replaced vacuous rfl proofs at uniform distribution permutation invariance, diagonal case, and off-diagonal case with explicit proof obligations and sorry. - section2_hermite_sieve.lean: Proved repunit strict monotonicity and lower bound lemmas, closing relevant sorry placeholders. - BindingSiteEntropy.lean: Swapped geodesicDistance placeholder with fisherRaoApprox and added counterexample sketch for fisher_implies_similar_druggability. - FixedPoint.lean, lakefile.lean, gemma4_mcp.py: Minor fixes and enhancements. - AGENTS.md: Tracked open Chentsov proof obligations. Build: 2987 jobs, 0 errors (lake build)
997 lines
41 KiB
Text
997 lines
41 KiB
Text
import Mathlib.Data.Matrix.Basic
|
||
import Mathlib.LinearAlgebra.Matrix.PosDef
|
||
import Mathlib.Data.Fin.Basic
|
||
import Mathlib.Analysis.Convex.Simplex
|
||
import Mathlib.Analysis.SpecialFunctions.Pow.Real
|
||
import Mathlib.Topology.Basic
|
||
import Mathlib.Data.Real.Basic
|
||
import Mathlib.Topology.Instances.Real
|
||
import Mathlib.Data.Rat.Basic
|
||
|
||
/-! ============================================================
|
||
ChentsovFinite.lean — Finite Chentsov Theorem for n=8
|
||
|
||
Proves that on the probability simplex Δ⁷ (8 outcomes),
|
||
the Fisher information metric is the UNIQUE Riemannian
|
||
metric (up to positive constant) that is invariant under
|
||
all Markov embeddings (stochastic refinements).
|
||
|
||
This is the mathematical foundation for the Hachimoji
|
||
geometry: the 8-state manifold has a CANONICAL metric,
|
||
not an arbitrary choice.
|
||
|
||
Proof outline:
|
||
1. Define probability simplex Δⁿ and tangent spaces
|
||
2. Define Markov embeddings (refinements of outcome space)
|
||
3. Define Fisher information metric
|
||
4. State Chentsov invariance condition
|
||
5. Prove the functional equation H̃(t) = q²H̃(qt) + (1-q)²H̃((1-q)t)
|
||
6. Solve: H̃(t) = c/t (unique continuous positive solution)
|
||
7. Prove Chentsov's theorem: g = c · g_Fisher
|
||
8. Instantiate n=8 and connect to HachimojiBase
|
||
============================================================ -/
|
||
|
||
open Real BigOperators Set
|
||
|
||
-- ============================================================
|
||
-- §1 PROBABILITY SIMPLEX AND TANGENT SPACE
|
||
-- ============================================================
|
||
|
||
section ProbabilitySimplex
|
||
|
||
/-- The open probability simplex on n outcomes:
|
||
Δⁿ⁻¹ = { p ∈ ℝⁿ | pᵢ > 0, Σ pᵢ = 1 } -/
|
||
def openSimplex (n : ℕ) : Set (Fin n → ℝ) :=
|
||
{ p | (∀ i, p i > 0) ∧ (∑ i, p i = 1) }
|
||
|
||
/-- Tangent space to Δⁿ⁻¹ at p: vectors whose components sum to 0. -/
|
||
def tangentSpace {n : ℕ} (p : openSimplex n) : Set (Fin n → ℝ) :=
|
||
{ X | ∑ i, X i = 0 }
|
||
|
||
/-- Tangent vector eᵢ - eⱼ (lies in tangent space). -/
|
||
def tangentBasis {n : ℕ} (i j : Fin n) : Fin n → ℝ :=
|
||
fun k => if k = i then 1 else if k = j then -1 else 0
|
||
|
||
lemma tangentBasis_sum {n : ℕ} (p : openSimplex n) (i j : Fin n) :
|
||
∑ k, tangentBasis i j k = 0 := by
|
||
simp [tangentBasis, Finset.sum_ite, Finset.filter_ne', Finset.sum_const]
|
||
<;> try { tauto }
|
||
|
||
lemma tangentBasis_in_tangentSpace {n : ℕ} (p : openSimplex n) (i j : Fin n) :
|
||
tangentBasis i j ∈ tangentSpace p := by
|
||
simp [tangentSpace, tangentBasis_sum]
|
||
|
||
end ProbabilitySimplex
|
||
|
||
|
||
-- ============================================================
|
||
-- §2 MARKOV EMBEDDINGS (STOCHASTIC REFINEMENTS)
|
||
-- ============================================================
|
||
|
||
section MarkovEmbeddings
|
||
|
||
/-- A splitting embedding refines a single outcome into two
|
||
sub-outcomes with conditional probabilities q and 1-q. -/
|
||
structure SplitEmbedding (n : ℕ) where
|
||
splitIdx : Fin n
|
||
q : ℝ
|
||
hq_pos : q > 0
|
||
hq_lt_one : q < 1
|
||
|
||
def SplitEmbedding.refinedSize {n : ℕ} (_ : SplitEmbedding n) : ℕ := n + 1
|
||
|
||
/-- Apply splitting embedding to a point in the simplex. -/
|
||
def SplitEmbedding.apply {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n) :
|
||
openSimplex (refinedSize f) :=
|
||
let q := f.q
|
||
let i₀ := f.splitIdx
|
||
⟨fun j =>
|
||
if j = ⟨0, by simp [refinedSize]⟩ then q * p.1 i₀
|
||
else if j = ⟨1, by simp [refinedSize]⟩ then (1 - q) * p.1 i₀
|
||
else p.1 (⟨j.1 - 1, by omega⟩ : Fin n),
|
||
by
|
||
constructor
|
||
· intro j
|
||
fin_cases j <;> simp [refinedSize] at *
|
||
· exact mul_pos f.hq_pos (p.2.1 i₀)
|
||
· exact mul_pos (sub_pos.mpr f.hq_lt_one) (p.2.1 i₀)
|
||
· exact p.2.1 _
|
||
· simp [refinedSize, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ]
|
||
have h1 : ∑ i : Fin n, p.1 i = 1 := p.2.2
|
||
simp_all [Finset.sum_range_succ]
|
||
<;> ring⟩
|
||
|
||
/-- Pushforward of tangent vectors under splitting embedding. -/
|
||
def SplitEmbedding.pushforward {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
|
||
(X : Fin n → ℝ) : Fin (refinedSize f) → ℝ :=
|
||
let q := f.q
|
||
let i₀ := f.splitIdx
|
||
fun j =>
|
||
if j = ⟨0, by simp [refinedSize]⟩ then q * X i₀
|
||
else if j = ⟨1, by simp [refinedSize]⟩ then (1 - q) * X i₀
|
||
else X (⟨j.1 - 1, by omega⟩ : Fin n)
|
||
|
||
lemma SplitEmbedding.pushforward_sum {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
|
||
(X : Fin n → ℝ) (hX : ∑ i, X i = 0) :
|
||
∑ j, f.pushforward p X j = 0 := by
|
||
simp [pushforward, refinedSize, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ]
|
||
rw [←hX]
|
||
ring_nf
|
||
simp [Finset.sum_range_succ]
|
||
<;> ring
|
||
|
||
lemma SplitEmbedding.pushforward_tangent {n : ℕ} (f : SplitEmbedding n) (p : openSimplex n)
|
||
(X : Fin n → ℝ) (hX : X ∈ tangentSpace p) :
|
||
f.pushforward p X ∈ tangentSpace (f.apply p) := by
|
||
simp [tangentSpace] at hX ⊢
|
||
exact f.pushforward_sum p X hX
|
||
|
||
end MarkovEmbeddings
|
||
|
||
|
||
-- ============================================================
|
||
-- §3 FISHER INFORMATION METRIC
|
||
-- ============================================================
|
||
|
||
section FisherMetric
|
||
|
||
/-- The Fisher information metric on the probability simplex. -/
|
||
noncomputable def fisherMetric {n : ℕ} (p : openSimplex n) (X Y : Fin n → ℝ) : ℝ :=
|
||
∑ i, X i * Y i / p.1 i
|
||
|
||
lemma fisherMetric_sym {n : ℕ} (p : openSimplex n) (X Y : Fin n → ℝ) :
|
||
fisherMetric p X Y = fisherMetric p Y X := by
|
||
simp [fisherMetric, mul_comm]
|
||
|
||
lemma fisherMetric_pos_def {n : ℕ} (p : openSimplex n) (X : Fin n → ℝ)
|
||
(hX : X ≠ 0) (hXsum : ∑ i, X i = 0) :
|
||
fisherMetric p X X > 0 := by
|
||
have h_pos : ∀ i, p.1 i > 0 := p.2.1
|
||
have h_ne : ∃ i, X i ≠ 0 := by
|
||
by_contra h
|
||
push_neg at h
|
||
have : X = 0 := by funext i; exact h i
|
||
contradiction
|
||
rcases h_ne with ⟨i₀, hi₀⟩
|
||
have h_term : X i₀ ^ 2 / p.1 i₀ > 0 := by
|
||
apply div_pos
|
||
· exact pow_two_pos_of_ne_zero hi₀
|
||
· exact h_pos i₀
|
||
have h_sum : fisherMetric p X X = ∑ i, X i ^ 2 / p.1 i := by
|
||
simp [fisherMetric, pow_two, mul_assoc]
|
||
rw [h_sum]
|
||
apply Finset.sum_pos
|
||
· intro i _
|
||
apply div_nonneg
|
||
· exact sq_nonneg (X i)
|
||
· exact le_of_lt (h_pos i)
|
||
· use i₀
|
||
simp
|
||
exact le_of_lt h_term
|
||
|
||
/-- Fisher metric is bilinear. -/
|
||
lemma fisherMetric_linear_left {n : ℕ} (p : openSimplex n) (Y : Fin n → ℝ) :
|
||
IsLinearMap ℝ (fun X => fisherMetric p X Y) := by
|
||
constructor
|
||
· intro x y
|
||
simp [fisherMetric, Finset.sum_add_distrib, add_mul]
|
||
ring
|
||
· intro c x
|
||
simp [fisherMetric, Finset.mul_sum, mul_assoc]
|
||
ring
|
||
|
||
lemma fisherMetric_linear_right {n : ℕ} (p : openSimplex n) (X : Fin n → ℝ) :
|
||
IsLinearMap ℝ (fun Y => fisherMetric p X Y) := by
|
||
constructor
|
||
· intro x y
|
||
simp [fisherMetric, Finset.sum_add_distrib, mul_add]
|
||
ring
|
||
· intro c y
|
||
simp [fisherMetric, Finset.mul_sum, mul_assoc]
|
||
ring
|
||
|
||
end FisherMetric
|
||
|
||
|
||
-- ============================================================
|
||
-- §4 CHENTSOV INVARIANCE
|
||
-- ============================================================
|
||
|
||
section ChentsovInvariance
|
||
|
||
/-- A Riemannian metric on the probability simplex. -/
|
||
structure RiemannianMetric (n : ℕ) where
|
||
toFun : (p : openSimplex n) → (X Y : Fin n → ℝ) → ℝ
|
||
linear_left : ∀ p Y, IsLinearMap ℝ (fun X => toFun p X Y)
|
||
linear_right : ∀ p X, IsLinearMap ℝ (fun Y => toFun p X Y)
|
||
symm : ∀ p X Y, toFun p X Y = toFun p Y X
|
||
pos_def : ∀ p X, X ≠ 0 → ∑ i, X i = 0 → toFun p X X > 0
|
||
|
||
/-- A metric is Chentsov-invariant if preserved under all
|
||
splitting Markov embeddings. -/
|
||
def IsChentsovInvariant {n : ℕ} (g : RiemannianMetric n) : Prop :=
|
||
∀ (f : SplitEmbedding n) (p : openSimplex n) (X Y : Fin n → ℝ),
|
||
∑ i, X i = 0 → ∑ i, Y i = 0 →
|
||
g.toFun p X Y = g.toFun (f.apply p) (f.pushforward p X) (f.pushforward p Y)
|
||
|
||
/-- Permutation invariance: g is unchanged when outcomes are relabelled.
|
||
|
||
This is a SEPARATE hypothesis from Chentsov invariance. In the classical
|
||
proof (Chentsov 1982, Campbell 1986), permutation invariance is either:
|
||
(a) assumed directly as part of the morphism class, or
|
||
(b) derived by showing the group generated by all Markov morphisms
|
||
(not just binary splittings) acts transitively on outcomes.
|
||
For SilverSight's binary-split model, it must be stated explicitly.
|
||
|
||
Concretely: if σ : Fin n ≃ Fin n is any permutation, and
|
||
σ_p i := p.1 (σ.symm i) (permuted distribution)
|
||
σ_X i := X (σ.symm i) (permuted tangent vector)
|
||
then g(σ_p, σ_X, σ_Y) = g(p, X, Y).
|
||
|
||
At the uniform distribution σ_p = p for all σ, so this implies
|
||
g_uniform(σ_X, σ_Y) = g_uniform(X, Y) — the key symmetry used in hc_pos. -/
|
||
def IsPermutationInvariant {n : ℕ} (g : RiemannianMetric n) : Prop :=
|
||
∀ (σ : Fin n ≃ Fin n) (p : openSimplex n) (X Y : Fin n → ℝ),
|
||
∑ i, X i = 0 → ∑ i, Y i = 0 →
|
||
let σp : openSimplex n :=
|
||
⟨fun i => p.1 (σ.symm i),
|
||
⟨fun i => p.2.1 (σ.symm i),
|
||
by simp [Finset.sum_equiv σ.symm (by simp) (by simp)]; exact p.2.2⟩⟩
|
||
g.toFun p X Y = g.toFun σp (fun i => X (σ.symm i)) (fun i => Y (σ.symm i))
|
||
|
||
end ChentsovInvariance
|
||
|
||
|
||
-- ============================================================
|
||
-- §5 FISHER METRIC IS CHENTSOV-INVARIANT
|
||
-- ============================================================
|
||
|
||
section FisherIsInvariant
|
||
|
||
/-- The Fisher metric is invariant under Markov embeddings. -/
|
||
lemma fisherMetric_chentsov_invariant {n : ℕ} :
|
||
IsChentsovInvariant
|
||
⟨fisherMetric, fisherMetric_linear_left, fisherMetric_linear_right,
|
||
fisherMetric_sym, fisherMetric_pos_def⟩ := by
|
||
intro f p X Y hXsum hYsum
|
||
simp [fisherMetric]
|
||
rcases f with ⟨i₀, q, hq_pos, hq_lt_one⟩
|
||
simp [SplitEmbedding.apply, SplitEmbedding.pushforward, SplitEmbedding.refinedSize]
|
||
simp_all [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ]
|
||
<;> ring_nf
|
||
<;> simp [Finset.sum_range_succ]
|
||
<;> ring
|
||
|
||
end FisherIsInvariant
|
||
|
||
|
||
-- ============================================================
|
||
-- §6 FUNCTIONAL EQUATION AND ITS UNIQUE SOLUTION
|
||
-- ============================================================
|
||
|
||
section FunctionalEquation
|
||
|
||
/-- The functional equation satisfied by the diagonal factor:
|
||
H(t) = q²·H(q·t) + (1-q)²·H((1-q)·t)
|
||
Derived from invariance under splitting an outcome. -/
|
||
def IsFunctionalEquation (H : ℝ → ℝ) : Prop :=
|
||
∀ (q : ℝ) (t : ℝ), q > 0 → q < 1 → t > 0 →
|
||
H t = q^2 * H (q * t) + (1 - q)^2 * H ((1 - q) * t)
|
||
|
||
/-- The substitution K(t) = t·H(t) linearizes the equation to:
|
||
K(t) = q·K(q·t) + (1-q)·K((1-q)·t) -/
|
||
lemma functional_eq_K {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H) :
|
||
let K := fun t => t * H t
|
||
∀ (q : ℝ) (t : ℝ), q > 0 → q < 1 → t > 0 →
|
||
K t = q * K (q * t) + (1 - q) * K ((1 - q) * t) := by
|
||
intro K q t hq_pos hq_lt_one ht_pos
|
||
have h1 := h_eq q t hq_pos hq_lt_one ht_pos
|
||
simp [K]
|
||
have h2 : q * (q * t * H (q * t)) + (1 - q) * ((1 - q) * t * H ((1 - q) * t))
|
||
= t * (q^2 * H (q * t) + (1 - q)^2 * H ((1 - q) * t)) := by ring
|
||
rw [h2, ←h1]
|
||
ring
|
||
|
||
/-- K(t) = K(t/2) for all t > 0 (using q = 1/2). -/
|
||
lemma functional_eq_K_half {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ t > 0, K t = K (t / 2) := by
|
||
intro t ht
|
||
have h1 := functional_eq_K h_eq
|
||
simp [hK] at h1 ⊢
|
||
specialize h1 (1 / 2) t (by norm_num) (by norm_num) ht
|
||
have h2 : (1 / 2 : ℝ) * ((1 / 2) * t * H ((1 / 2) * t))
|
||
+ (1 - (1 / 2 : ℝ)) * ((1 - (1 / 2 : ℝ)) * t * H ((1 - (1 / 2 : ℝ)) * t))
|
||
= (1 / 2) * t * H (t / 2) + (1 / 2) * t * H (t / 2) := by
|
||
ring_nf
|
||
rw [h2] at h1
|
||
have h3 : (1 / 2 : ℝ) * t * H (t / 2) + (1 / 2) * t * H (t / 2)
|
||
= t * H (t / 2) := by ring
|
||
rw [h3] at h1
|
||
rw [h1]
|
||
ring
|
||
|
||
/-- K(t) = K(t/2ⁿ) for all n ≥ 0. -/
|
||
lemma functional_eq_K_pow {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ (n : ℕ) (t > 0), K t = K (t / 2^n) := by
|
||
intro n
|
||
induction n with
|
||
| zero => simp
|
||
| succ n ih =>
|
||
intro t ht
|
||
have h1 : K t = K (t / 2^n) := ih t ht
|
||
have h2 : K (t / 2^n) = K ((t / 2^n) / 2) :=
|
||
functional_eq_K_half h_eq hK (t / 2^n) (by positivity)
|
||
have h3 : (t / 2^n : ℝ) / 2 = t / 2^(n + 1 : ℕ) := by ring_nf
|
||
rw [h1, h2, h3]
|
||
|
||
/-- K(t) = K(2t) for all t > 0. -/
|
||
lemma functional_eq_K_double {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ t > 0, K t = K (2 * t) := by
|
||
intro t ht
|
||
have h1 : K (2 * t) = K ((2 * t) / 2) :=
|
||
functional_eq_K_half h_eq hK (2 * t) (by linarith)
|
||
have h2 : (2 * t : ℝ) / 2 = t := by ring
|
||
rw [h2] at h1
|
||
rw [h1]
|
||
|
||
/-- K(t) = K(m·t) for all positive integers m. -/
|
||
lemma functional_eq_K_int_mul {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ (m : ℕ) (t > 0), m > 0 → K t = K (m * t) := by
|
||
intro m t ht hm
|
||
induction m with
|
||
| zero => linarith
|
||
| succ m ih =>
|
||
cases m with
|
||
| zero => simp
|
||
| succ m =>
|
||
have h1 : K t = K ((m + 1 : ℕ) * t) := ih (by linarith) (by linarith)
|
||
have h2 : K ((m + 1 : ℕ) * t) = K ((m + 2 : ℕ) * t) := by
|
||
have h3 : K ((m + 2 : ℕ) * t) = K (((m + 2 : ℕ) * t) / 2) :=
|
||
functional_eq_K_half h_eq hK ((m + 2 : ℕ) * t)
|
||
(by positivity)
|
||
have h4 : K ((m + 1 : ℕ) * t) = K (((m + 1 : ℕ) * t) / 2) :=
|
||
functional_eq_K_half h_eq hK ((m + 1 : ℕ) * t)
|
||
(by positivity)
|
||
-- Use the functional equation with q = (m+1)/(m+2)
|
||
have h6 := functional_eq_K h_eq
|
||
simp [hK] at h6
|
||
specialize h6 ((m + 1 : ℝ) / (m + 2)) ((m + 2 : ℕ) * t)
|
||
(by positivity) (by
|
||
have h7 : (m + 1 : ℝ) < (m + 2 : ℝ) := by linarith
|
||
have h8 : (m + 1 : ℝ) / (m + 2) < 1 := by
|
||
apply (div_lt_one (by positivity)).mpr h7
|
||
exact h8
|
||
) (by positivity)
|
||
have h7 : (m + 1 : ℝ) / (m + 2) * ((m + 2 : ℕ) * t) = (m + 1 : ℕ) * t := by
|
||
field_simp; ring
|
||
have h8 : (1 - (m + 1 : ℝ) / (m + 2)) * ((m + 2 : ℕ) * t) = t := by
|
||
have h9 : 1 - (m + 1 : ℝ) / (m + 2) = 1 / (m + 2) := by
|
||
field_simp; ring
|
||
rw [h9]
|
||
field_simp; ring
|
||
simp [h7, h8] at h6
|
||
have h9 : K ((m + 2 : ℕ) * t) = K ((m + 1 : ℕ) * t) := by
|
||
linarith [h6]
|
||
exact h9.symm
|
||
rw [h1, h2]
|
||
|
||
/-- K(t/m) = K(t) for all positive integers m. -/
|
||
lemma functional_eq_K_div {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ (m : ℕ) (t > 0), m > 0 → K (t / m) = K t := by
|
||
intro m t ht hm
|
||
have h1 := functional_eq_K_int_mul h_eq hK m (t / m)
|
||
(by positivity) hm
|
||
have h2 : (m : ℝ) * (t / m) = t := by
|
||
field_simp
|
||
<;> ring
|
||
rw [h2] at h1
|
||
exact h1.symm
|
||
|
||
/-- K(rt) = K(t) for all positive rationals r. -/
|
||
lemma functional_eq_K_rat {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t) :
|
||
∀ (r : ℚ) (t > 0), r > 0 → K (r * t) = K t := by
|
||
intro r t ht hr
|
||
have hr_num : r.num > 0 := by
|
||
have h1 : (r.num : ℚ) > 0 := by
|
||
have h2 : (r.num : ℚ) = r * r.den := by
|
||
have h3 : (r.den : ℚ) > 0 := by exact_mod_cast r.pos
|
||
field_simp
|
||
<;> rw [Rat.mul_den_eq_num]
|
||
rw [h2]
|
||
nlinarith [hr, show (r.den : ℚ) > 0 by exact_mod_cast r.pos]
|
||
exact_mod_cast h1
|
||
have h1 : K ((r.num : ℝ) * (t / r.den)) = K (t / r.den) :=
|
||
functional_eq_K_int_mul h_eq hK r.num (t / r.den)
|
||
(by positivity) hr_num
|
||
have h2 : (r.num : ℝ) * (t / r.den) = r * t := by
|
||
have h3 : (r : ℝ) = (r.num : ℝ) / r.den := by
|
||
have h4 : (r.den : ℝ) > 0 := by exact_mod_cast r.pos
|
||
field_simp
|
||
<;> norm_num
|
||
<;> rw [Rat.cast_def]
|
||
<;> field_simp
|
||
rw [h3]
|
||
ring_nf
|
||
<;> field_simp
|
||
<;> ring
|
||
have h3 : K (t / r.den) = K t :=
|
||
functional_eq_K_div h_eq hK r.den t ht r.pos
|
||
rw [h2, h1, h3]
|
||
|
||
/-- **Key Lemma:** If H satisfies the functional equation and
|
||
K(t) = t·H(t) is continuous on (0,∞), then K is constant.
|
||
Proof: K(rt) = K(t) for all positive rationals r,
|
||
and by density of ℚ in ℝ and continuity, K is constant. -/
|
||
lemma functional_eq_K_const {H : ℝ → ℝ} (h_eq : IsFunctionalEquation H)
|
||
{K : ℝ → ℝ} (hK : K = fun t => t * H t)
|
||
(h_cont : ContinuousOn K (Ioi 0)) :
|
||
∃ (c : ℝ), ∀ t > 0, K t = c := by
|
||
use K 1
|
||
intro t ht
|
||
have h_local_const : ∀ (r : ℚ) (s > 0), r > 0 → K (r * s) = K s :=
|
||
functional_eq_K_rat h_eq hK
|
||
have h_seq : ∃ (r : ℕ → ℚ), (∀ n, r n > 0) ∧
|
||
Filter.Tendsto (fun n => (r n : ℝ)) Filter.atTop (nhds t) := by
|
||
have h1 : ∃ (r : ℕ → ℚ), Filter.Tendsto (fun n => (r n : ℝ)) Filter.atTop (nhds t) := by
|
||
apply Rat.denseRange_cast.exists_seq_tendsto
|
||
simp [ht]
|
||
rcases h1 with ⟨r, hr⟩
|
||
use fun n => max (r n) (1 / (n + 1 : ℚ))
|
||
constructor
|
||
· intro n
|
||
simp [show (1 / (n + 1 : ℚ) : ℝ) > 0 by positivity]
|
||
· have h2 : Filter.Tendsto (fun n => max ((r n : ℝ)) (1 / (n + 1 : ℝ)))
|
||
Filter.atTop (nhds (max t 0)) := by
|
||
apply Filter.Tendsto.max
|
||
· exact hr
|
||
· have h3 : Filter.Tendsto (fun n : ℕ => (1 / (n + 1 : ℝ) : ℝ))
|
||
Filter.atTop (nhds 0) := by
|
||
have h4 : Filter.Tendsto (fun n : ℕ => (n + 1 : ℝ)) Filter.atTop
|
||
Filter.atTop := by
|
||
apply Filter.tendsto_atTop_atTop_of_monotone
|
||
· intro a b hab; simp [hab]
|
||
· intro a; use a; simp
|
||
have h5 : Filter.Tendsto (fun n : ℕ => (1 / (n + 1 : ℝ) : ℝ))
|
||
Filter.atTop (nhds 0) := by
|
||
apply Tendsto.inv_tendsto_atTop
|
||
exact h4
|
||
exact h5
|
||
have h4 : nhds (max t 0) = nhds t := by
|
||
rw [max_eq_left]
|
||
linarith [ht]
|
||
rw [h4]
|
||
exact h3
|
||
have h3 : max t 0 = t := by apply max_eq_left; linarith [ht]
|
||
rw [h3] at h2
|
||
exact h2
|
||
rcases h_seq with ⟨r, hr_pos, hr_tendsto⟩
|
||
have h_K_r : ∀ n, K ((r n : ℝ) * (1 : ℝ)) = K (1 : ℝ) := by
|
||
intro n
|
||
apply h_local_const
|
||
exact hr_pos n
|
||
norm_num
|
||
have h2 : Filter.Tendsto (fun n => K ((r n : ℝ) * (1 : ℝ))) Filter.atTop
|
||
(nhds (K t)) := by
|
||
have h3 : (fun n => (r n : ℝ) * (1 : ℝ)) = (fun n => (r n : ℝ)) := by
|
||
funext n; ring
|
||
rw [h3]
|
||
apply ContinuousAt.tendsto
|
||
apply ContinuousOn.continuousAt h_cont
|
||
simp [ht]
|
||
have h3 : Filter.Tendsto (fun n => K ((r n : ℝ) * (1 : ℝ))) Filter.atTop
|
||
(nhds (K (1 : ℝ))) := by
|
||
have h4 : ∀ n, K ((r n : ℝ) * (1 : ℝ)) = K (1 : ℝ) := h_K_r
|
||
have h5 : (fun n => K ((r n : ℝ) * (1 : ℝ))) = (fun _ => K (1 : ℝ)) := by
|
||
funext n
|
||
exact h4 n
|
||
rw [h5]
|
||
exact tendsto_const_nhds
|
||
have h4 : K t = K (1 : ℝ) := by
|
||
apply tendsto_nhds_unique h2 h3
|
||
exact h4
|
||
|
||
/-- **Uniqueness Theorem:** The functional equation
|
||
H(t) = q²·H(q·t) + (1-q)²·H((1-q)·t)
|
||
has a unique continuous positive solution: H(t) = c/t. -/
|
||
theorem functional_eq_unique {H : ℝ → ℝ}
|
||
(h_eq : IsFunctionalEquation H)
|
||
(h_cont : ContinuousOn H (Ioi 0))
|
||
(h_pos : ∀ t > 0, H t > 0) :
|
||
∃ (c : ℝ), c > 0 ∧ ∀ t > 0, H t = c / t := by
|
||
let K : ℝ → ℝ := fun t => t * H t
|
||
have hK : K = fun t => t * H t := rfl
|
||
have hK_cont : ContinuousOn K (Ioi 0) := by
|
||
simp [hK]
|
||
apply ContinuousOn.mul
|
||
· apply continuousOn_id
|
||
· exact h_cont
|
||
rcases functional_eq_K_const h_eq hK hK_cont with ⟨c, hc⟩
|
||
use c
|
||
constructor
|
||
· have h1 := h_pos 1 (by norm_num)
|
||
have h2 : K 1 = c := hc 1 (by norm_num)
|
||
simp [hK] at h2
|
||
nlinarith
|
||
· intro t ht
|
||
have h1 : K t = c := hc t ht
|
||
simp [hK] at h1
|
||
have ht_ne : t ≠ 0 := by linarith
|
||
field_simp
|
||
linarith
|
||
|
||
end FunctionalEquation
|
||
|
||
|
||
-- ============================================================
|
||
-- §7 CHENTSOV'S THEOREM (Main Result)
|
||
-- ============================================================
|
||
|
||
section ChentsovTheorem
|
||
|
||
/-- **Chentsov's Theorem (Finite Version).**
|
||
Let g be a Riemannian metric on the (n-1)-dimensional
|
||
probability simplex with n ≥ 3 outcomes. If g is invariant
|
||
under all splitting Markov embeddings, then g = c · g_Fisher.
|
||
|
||
The constant c is determined by evaluating g at the uniform
|
||
distribution on the basis vector e₁ - e₀. -/
|
||
/-- **Chentsov's Theorem (Finite Version) — INCOMPLETE.**
|
||
|
||
Status: Three proof obligations remain open (marked `sorry`):
|
||
|
||
1. `h9` (line ~589): diagonal entries of g at the uniform distribution are
|
||
permutation-symmetric. Requires `h_perm` at σ = Equiv.swap 1 2.
|
||
**This sorry is closable** given `h_perm`; the proof is indicated below.
|
||
|
||
2. `h_agree` diagonal case: g(eᵢ-e₀, eᵢ-e₀) = c_val·(1/pᵢ + 1/p₀).
|
||
**Proof obligation:** apply h_inv at splitIdx=i with parameter q, expand
|
||
the pushforward, derive the functional equation for H(t)=g_p(eᵢ-e₀,eᵢ-e₀)
|
||
when p_i=t, then invoke `functional_eq_unique` to get H(t)=c/t.
|
||
|
||
3. `h_agree` off-diagonal case: g(eᵢ-e₀, eⱼ-e₀) = c_val/p₀.
|
||
**Proof obligation:** apply h_inv at splitIdx=0 (splitting the reference
|
||
outcome) and use the resulting functional equation for the cross term.
|
||
|
||
The bilinearity expansion (h_expand_g, h_expand_f) and the functional
|
||
equation uniqueness theorem (`functional_eq_unique`) are both correctly
|
||
proven. Only the CONNECTION between h_inv and h_agree is missing.
|
||
|
||
TODO(lean-port): close the three sorries; estimated ~200 lines of tactic.
|
||
Reference: Campbell (1986) "An extended Čencov characterization",
|
||
AMS Proc. 54:135-141. -/
|
||
theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
|
||
(h_inv : IsChentsovInvariant g)
|
||
(h_perm : IsPermutationInvariant g) -- new: permutation invariance
|
||
(h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex n =>
|
||
g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) :
|
||
∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ),
|
||
(∑ i, X i = 0) → (∑ i, Y i = 0) →
|
||
g.toFun p X Y = c * fisherMetric p X Y := by
|
||
|
||
-- **Step 1: Define the uniform distribution and extract c.**
|
||
let u : Fin n → ℝ := fun _ => 1 / n
|
||
have hn_pos : n > 0 := by linarith
|
||
have hu : u ∈ openSimplex n := by
|
||
constructor
|
||
· intro i
|
||
simp [u]
|
||
positivity
|
||
· simp [u]
|
||
field_simp
|
||
let u_op : openSimplex n := ⟨u, hu⟩
|
||
|
||
-- At the uniform distribution, permutation invariance forces
|
||
-- G_ij(u) = a if i=j, G_ij(u) = b if i≠j (for i,j ≥ 1).
|
||
-- The constant c = a - b > 0 by positive definiteness.
|
||
let c_val : ℝ := g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0)
|
||
- g.toFun u_op (tangentBasis 1 0) (tangentBasis 2 0)
|
||
|
||
have hc_pos : c_val > 0 := by
|
||
have h1 : tangentBasis 1 0 ≠ 0 := by
|
||
intro h
|
||
have h2 := congr_fun h 1
|
||
simp [tangentBasis] at h2
|
||
have h2 : ∑ i : Fin n, tangentBasis 1 0 i = 0 :=
|
||
tangentBasis_sum u_op 1 0
|
||
have h3 : g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0) > 0 :=
|
||
g.pos_def u_op (tangentBasis 1 0) h1 h2
|
||
-- Show c_val = g(V, V) where V = e_1 - e_2, which is > 0
|
||
have h4 : c_val = g.toFun u_op (tangentBasis 1 2) (tangentBasis 1 2) := by
|
||
have h5 : tangentBasis 1 2 = tangentBasis 1 0 - tangentBasis 2 0 := by
|
||
funext k
|
||
simp [tangentBasis]
|
||
by_cases h1 : k = 1 <;> by_cases h2 : k = 2 <;> by_cases h0 : k = 0
|
||
all_goals simp [h1, h2, h0]
|
||
all_goals tauto
|
||
rw [h5]
|
||
have h6 : IsLinearMap ℝ (fun X => g.toFun u_op X (tangentBasis 1 0 - tangentBasis 2 0)) := by
|
||
have h7 : IsLinearMap ℝ (fun X => g.toFun u_op X (tangentBasis 1 0 - tangentBasis 2 0)) :=
|
||
g.linear_left u_op (tangentBasis 1 0 - tangentBasis 2 0)
|
||
exact h7
|
||
have h7 : g.toFun u_op (tangentBasis 1 0 - tangentBasis 2 0) (tangentBasis 1 0 - tangentBasis 2 0)
|
||
= g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0)
|
||
- g.toFun u_op (tangentBasis 1 0) (tangentBasis 2 0)
|
||
- g.toFun u_op (tangentBasis 2 0) (tangentBasis 1 0)
|
||
+ g.toFun u_op (tangentBasis 2 0) (tangentBasis 2 0) := by
|
||
have h8 : IsLinearMap ℝ (fun Y => g.toFun u_op (tangentBasis 1 0) Y) :=
|
||
g.linear_right u_op (tangentBasis 1 0)
|
||
have h9 : IsLinearMap ℝ (fun Y => g.toFun u_op (tangentBasis 2 0) Y) :=
|
||
g.linear_right u_op (tangentBasis 2 0)
|
||
simp [IsLinearMap.map_sub, h8, h9]
|
||
ring
|
||
rw [h7]
|
||
have h8 : g.toFun u_op (tangentBasis 2 0) (tangentBasis 1 0)
|
||
= g.toFun u_op (tangentBasis 1 0) (tangentBasis 2 0) :=
|
||
g.symm u_op (tangentBasis 2 0) (tangentBasis 1 0)
|
||
rw [h8]
|
||
-- At uniform distribution, diagonal entries are equal.
|
||
-- Proof: apply h_perm with σ = Equiv.swap 1 2.
|
||
-- σ_p = u_op because uniform is permutation-invariant.
|
||
-- σ(tangentBasis 1 0) = tangentBasis 2 0 (swapping indices 1 and 2).
|
||
-- So h_perm gives: g(u_op, e₁-e₀, e₁-e₀) = g(σ_p, e₂-e₀, e₂-e₀)
|
||
-- = g(u_op, e₂-e₀, e₂-e₀). ∎
|
||
have h9 : g.toFun u_op (tangentBasis 2 0) (tangentBasis 2 0)
|
||
= g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0) := by
|
||
have hswap_sum1 : ∑ i : Fin n, tangentBasis 1 0 i = 0 :=
|
||
tangentBasis_sum u_op 1 0
|
||
have hswap_sum2 : ∑ i : Fin n, tangentBasis 2 0 i = 0 :=
|
||
tangentBasis_sum u_op 2 0
|
||
-- Apply permutation invariance with σ = Equiv.swap 1 2
|
||
have h_apply := h_perm (Equiv.swap 1 2) u_op
|
||
(tangentBasis 1 0) (tangentBasis 1 0) hswap_sum1 hswap_sum1
|
||
-- After σ, the uniform distribution is still uniform (permutation-stable)
|
||
-- and σ(tangentBasis 1 0) = tangentBasis 2 0.
|
||
-- TODO(lean-port): unfold h_apply and verify the σ_p = u_op equality
|
||
-- (uniform distribution is fixed by all permutations) and the
|
||
-- reindexing (Equiv.swap 1 2).symm ≫ tangentBasis 1 0 = tangentBasis 2 0).
|
||
-- This closes with ~20 lines of simp/funext once h_apply is unfolded.
|
||
sorry -- closable via h_perm; proof sketch above
|
||
rw [h9]
|
||
ring
|
||
rw [h4]
|
||
have h5 : tangentBasis 1 2 ≠ 0 := by
|
||
intro h
|
||
have h2 := congr_fun h 1
|
||
simp [tangentBasis] at h2
|
||
have h6 : ∑ i : Fin n, tangentBasis 1 2 i = 0 :=
|
||
tangentBasis_sum u_op 1 2
|
||
apply g.pos_def
|
||
· exact h5
|
||
· exact h6
|
||
|
||
-- **Step 2: Show g = c_val · g_Fisher on basis vectors.**
|
||
-- For any point p and indices i, j ≥ 1:
|
||
-- g_p(e_i - e_0, e_j - e_0) = c_val · (δ_ij/p_i + 1/p_0)
|
||
|
||
-- This is proved using:
|
||
-- (a) Permutation invariance → structure G_ij(p) = δ_ij·H(p_i) + K(p_0)
|
||
-- (b) Embedding invariance → functional equation for H
|
||
-- (c) Uniqueness theorem → H(t) = c_val/t, K(s) = c_val/s
|
||
|
||
-- **Step 3: Extend by linearity to all tangent vectors.**
|
||
|
||
use c_val, hc_pos
|
||
|
||
intro p X Y hXsum hYsum
|
||
|
||
-- Basis expansion: X = Σ_{i=1}^{n-1} X_i (e_i - e_0)
|
||
have h_basis_X : X = ∑ i in Finset.univ.erase 0, X i • tangentBasis i 0 := by
|
||
funext k
|
||
simp [tangentBasis, Finset.sum_erase_univ]
|
||
by_cases hk : k = 0
|
||
· rw [hk]
|
||
have h_sum0 : X 0 = - ∑ i in Finset.univ.erase 0, X i := by
|
||
have h_total : ∑ i, X i = 0 := hXsum
|
||
simp [Finset.sum_erase_add] at h_total
|
||
linarith
|
||
simp [h_sum0]
|
||
ring
|
||
· simp [hk]
|
||
by_cases hk2 : k = 0
|
||
· tauto
|
||
· simp [hk2]
|
||
|
||
have h_basis_Y : Y = ∑ j in Finset.univ.erase 0, Y j • tangentBasis j 0 := by
|
||
funext k
|
||
simp [tangentBasis, Finset.sum_erase_univ]
|
||
by_cases hk : k = 0
|
||
· rw [hk]
|
||
have h_sum0 : Y 0 = - ∑ j in Finset.univ.erase 0, Y j := by
|
||
have h_total : ∑ j, Y j = 0 := hYsum
|
||
simp [Finset.sum_erase_add] at h_total
|
||
linarith
|
||
simp [h_sum0]
|
||
ring
|
||
· simp [hk]
|
||
by_cases hk2 : k = 0
|
||
· tauto
|
||
· simp [hk2]
|
||
|
||
-- Expand both sides using bilinearity
|
||
have h_expand_g : g.toFun p X Y = ∑ i in Finset.univ.erase 0,
|
||
∑ j in Finset.univ.erase 0, X i * Y j * g.toFun p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
rw [h_basis_X, h_basis_Y]
|
||
simp [Finset.sum_mul, Finset.mul_sum, mul_assoc]
|
||
-- Use linearity of g
|
||
congr
|
||
funext i
|
||
congr
|
||
funext j
|
||
have h_lin : g.toFun p (X i • tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= X i * Y j * g.toFun p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
have h1 : IsLinearMap ℝ (fun X' => g.toFun p X' (Y j • tangentBasis j 0)) :=
|
||
g.linear_left p (Y j • tangentBasis j 0)
|
||
have h2 : IsLinearMap ℝ (fun Y' => g.toFun p (tangentBasis i 0) Y') :=
|
||
g.linear_right p (tangentBasis i 0)
|
||
have h3 : g.toFun p (X i • tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= X i * g.toFun p (tangentBasis i 0) (Y j • tangentBasis j 0) := by
|
||
have h4 : (X i • tangentBasis i 0) = (fun k => X i * tangentBasis i 0 k) := rfl
|
||
rw [h4]
|
||
have h5 : g.toFun p (fun k : Fin n => X i * tangentBasis i 0 k) (Y j • tangentBasis j 0)
|
||
= X i * g.toFun p (tangentBasis i 0) (Y j • tangentBasis j 0) := by
|
||
have h6 : IsLinearMap ℝ (fun X'' => g.toFun p X'' (Y j • tangentBasis j 0)) :=
|
||
g.linear_left p (Y j • tangentBasis j 0)
|
||
have h7 : (fun k : Fin n => X i * tangentBasis i 0 k)
|
||
= X i • (fun k => tangentBasis i 0 k) := rfl
|
||
rw [h7]
|
||
exact IsLinearMap.map_smul h6 (tangentBasis i 0) X i
|
||
exact h5
|
||
have h4 : g.toFun p (tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= Y j * g.toFun p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
have h5 : (Y j • tangentBasis j 0) = (fun k => Y j * tangentBasis j 0 k) := rfl
|
||
rw [h5]
|
||
have h6 : IsLinearMap ℝ (fun Y'' => g.toFun p (tangentBasis i 0) Y'') :=
|
||
g.linear_right p (tangentBasis i 0)
|
||
have h7 : (fun k : Fin n => Y j * tangentBasis j 0 k)
|
||
= Y j • (fun k => tangentBasis j 0 k) := rfl
|
||
rw [h7]
|
||
exact IsLinearMap.map_smul h6 (tangentBasis j 0) Y j
|
||
rw [h3, h4]
|
||
exact h_lin
|
||
|
||
have h_expand_f : fisherMetric p X Y = ∑ i in Finset.univ.erase 0,
|
||
∑ j in Finset.univ.erase 0, X i * Y j * fisherMetric p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
rw [h_basis_X, h_basis_Y]
|
||
simp [Finset.sum_mul, Finset.mul_sum, mul_assoc]
|
||
congr
|
||
funext i
|
||
congr
|
||
funext j
|
||
have h_lin : fisherMetric p (X i • tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= X i * Y j * fisherMetric p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
have h1 : IsLinearMap ℝ (fun X' => fisherMetric p X' (Y j • tangentBasis j 0)) :=
|
||
fisherMetric_linear_left p (Y j • tangentBasis j 0)
|
||
have h2 : IsLinearMap ℝ (fun Y' => fisherMetric p (tangentBasis i 0) Y') :=
|
||
fisherMetric_linear_right p (tangentBasis i 0)
|
||
have h3 : fisherMetric p (X i • tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= X i * fisherMetric p (tangentBasis i 0) (Y j • tangentBasis j 0) := by
|
||
have h4 : (X i • tangentBasis i 0) = (fun k => X i * tangentBasis i 0 k) := rfl
|
||
rw [h4]
|
||
have h5 : fisherMetric p (fun k : Fin n => X i * tangentBasis i 0 k) (Y j • tangentBasis j 0)
|
||
= X i * fisherMetric p (tangentBasis i 0) (Y j • tangentBasis j 0) := by
|
||
have h6 : IsLinearMap ℝ (fun X'' => fisherMetric p X'' (Y j • tangentBasis j 0)) :=
|
||
fisherMetric_linear_left p (Y j • tangentBasis j 0)
|
||
have h7 : (fun k : Fin n => X i * tangentBasis i 0 k)
|
||
= X i • (fun k => tangentBasis i 0 k) := rfl
|
||
rw [h7]
|
||
exact IsLinearMap.map_smul h6 (tangentBasis i 0) X i
|
||
exact h5
|
||
have h4 : fisherMetric p (tangentBasis i 0) (Y j • tangentBasis j 0)
|
||
= Y j * fisherMetric p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
have h5 : (Y j • tangentBasis j 0) = (fun k => Y j * tangentBasis j 0 k) := rfl
|
||
rw [h5]
|
||
have h6 : IsLinearMap ℝ (fun Y'' => fisherMetric p (tangentBasis i 0) Y'') :=
|
||
fisherMetric_linear_right p (tangentBasis i 0)
|
||
have h7 : (fun k : Fin n => Y j * tangentBasis j 0 k)
|
||
= Y j • (fun k => tangentBasis j 0 k) := rfl
|
||
rw [h7]
|
||
exact IsLinearMap.map_smul h6 (tangentBasis j 0) Y j
|
||
rw [h3, h4]
|
||
exact h_lin
|
||
|
||
-- Key: g and c_val·g_Fisher agree on basis vectors
|
||
have h_agree : ∀ (i j : Fin n), i ≠ 0 → j ≠ 0 →
|
||
g.toFun p (tangentBasis i 0) (tangentBasis j 0)
|
||
= c_val * fisherMetric p (tangentBasis i 0) (tangentBasis j 0) := by
|
||
intro i j hi hj
|
||
by_cases hij : i = j
|
||
· -- Diagonal: g(eᵢ-e₀, eᵢ-e₀) = c_val · (1/p_i + 1/p_0)
|
||
-- PROOF OBLIGATION (connects h_inv → functional_eq_unique → diagonal form):
|
||
--
|
||
-- Step A. Define H : ℝ → ℝ by H(t) := g_{p[i←t]}(eᵢ-e₀, eᵢ-e₀)
|
||
-- where p[i←t] is p with the i-th coordinate set to t.
|
||
-- (This requires p to vary continuously; use h_smooth.)
|
||
--
|
||
-- Step B. Apply h_inv with (splitIdx := i, q := q) for arbitrary q ∈ (0,1).
|
||
-- The invariance equation unfolds to:
|
||
-- g_p(eᵢ-e₀, eᵢ-e₀) = q²·g_{f(p)}(eᵢ'-e₀', eᵢ'-e₀')
|
||
-- + (1-q)²·g_{f(p)}(eᵢ''-e₀', eᵢ''-e₀')
|
||
-- + cross terms (vanish by off-diagonal = 0,
|
||
-- shown in the off-diagonal case below)
|
||
-- This gives: H(p_i) = q²·H(q·p_i) + (1-q)²·H((1-q)·p_i)
|
||
-- i.e. H satisfies `IsFunctionalEquation`.
|
||
--
|
||
-- Step C. H is continuous on (0,1) ⊂ (0,∞) by h_smooth.
|
||
-- H is positive by g.pos_def.
|
||
-- Apply `functional_eq_unique`: ∃ c, H(t) = c/t.
|
||
--
|
||
-- Step D. Evaluate at t = 1/n (uniform distribution, p_i = 1/n):
|
||
-- H(1/n) = c / (1/n) = c·n
|
||
-- But also H(1/n) = g_{u_op}(eᵢ-e₀, eᵢ-e₀) = g_{u_op}(e₁-e₀, e₁-e₀)
|
||
-- by h_perm (permutation invariance at uniform).
|
||
-- And g_{u_op}(e₁-e₀, e₁-e₀) = c_val + g_{u_op}(e₁-e₀, e₂-e₀)
|
||
-- Solving: c = c_val (the constant defined at the top).
|
||
--
|
||
-- Step E. Therefore H(t) = c_val/t, so:
|
||
-- g_p(eᵢ-e₀, eᵢ-e₀) = c_val/p_i + c_val/p_0
|
||
-- = c_val · (1/p_i + 1/p_0)
|
||
-- = c_val · fisherMetric p (eᵢ-e₀) (eᵢ-e₀)
|
||
rw [hij]
|
||
simp only [fisherMetric, tangentBasis]
|
||
sorry -- TODO(lean-port): Steps A–E above; uses functional_eq_unique
|
||
· -- Off-diagonal: g(eᵢ-e₀, eⱼ-e₀) = c_val/p_0 (i ≠ j, i,j ≠ 0)
|
||
-- PROOF OBLIGATION:
|
||
--
|
||
-- Step A. Apply h_inv with (splitIdx := 0, q := q) — split the reference
|
||
-- outcome e₀ into two sub-outcomes.
|
||
-- The pushforward maps:
|
||
-- eᵢ-e₀ ↦ eᵢ - q·e₀' - (1-q)·e₀''
|
||
-- eⱼ-e₀ ↦ eⱼ - q·e₀' - (1-q)·e₀''
|
||
--
|
||
-- Step B. Expand invariance equation; diagonal terms cancel (by Step A
|
||
-- of the diagonal case); cross terms give:
|
||
-- g_p(eᵢ-e₀, eⱼ-e₀) = q²·g_{f(p)}(eᵢ-e₀', eⱼ-e₀')
|
||
-- + (1-q)²·g_{f(p)}(eᵢ-e₀'', eⱼ-e₀'')
|
||
-- + q(1-q)·[ g_{f(p)}(eᵢ-e₀', eⱼ-e₀'')
|
||
-- + g_{f(p)}(eᵢ-e₀'', eⱼ-e₀') ]
|
||
-- Define K(s) := g_{p[0←s]}(eᵢ-e₀, eⱼ-e₀); this satisfies the
|
||
-- same functional equation as H.
|
||
--
|
||
-- Step C. Apply `functional_eq_unique` → K(s) = c'/s for some c' > 0.
|
||
-- Evaluate at s = 1/n and use h_perm: c' = c_val.
|
||
-- Therefore g_p(eᵢ-e₀, eⱼ-e₀) = c_val/p_0
|
||
-- = c_val · fisherMetric p (eᵢ-e₀) (eⱼ-e₀)
|
||
-- (since fisherMetric p (eᵢ-e₀) (eⱼ-e₀) = 1/p₀ for i≠j, i,j≠0)
|
||
simp only [fisherMetric, tangentBasis, hij]
|
||
sorry -- TODO(lean-port): Steps A–C above; uses functional_eq_unique
|
||
|
||
-- Combine to show g = c_val · g_Fisher
|
||
rw [h_expand_g, h_expand_f]
|
||
simp_rw [h_agree]
|
||
simp [Finset.mul_sum]
|
||
<;> ring
|
||
|
||
-- NOTE: chentsov_theorem_complete now requires h_perm (IsPermutationInvariant).
|
||
-- This propagates the additional hypothesis made explicit by the sorry-fix.
|
||
-- Callers must supply both h_inv and h_perm; see chentsov_theorem docstring.
|
||
theorem chentsov_theorem_complete (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
|
||
(h_inv : IsChentsovInvariant g)
|
||
(h_perm : IsPermutationInvariant g)
|
||
(h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex n =>
|
||
g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) :
|
||
∃ (c : ℝ), c > 0 ∧ ∀ (p : openSimplex n) (X Y : Fin n → ℝ),
|
||
(∑ i, X i = 0) → (∑ i, Y i = 0) →
|
||
g.toFun p X Y = c * fisherMetric p X Y := by
|
||
exact chentsov_theorem n hn g h_inv h_perm h_smooth
|
||
|
||
end ChentsovTheorem
|
||
|
||
|
||
-- ============================================================
|
||
-- §8 HACHIMOJI 8-STATE SYSTEM
|
||
-- ============================================================
|
||
|
||
section HachimojiConnection
|
||
|
||
/-- The 8 Hachimoji states classify lattice points by their
|
||
|Λ(m,n)| value relative to the Baker threshold. -/
|
||
inductive HachimojiBase where
|
||
| A -- trivial: |Λ| >> B^{-C}
|
||
| T -- room: |Λ| > 2·B^{-C}
|
||
| G -- tight: B^{-C} < |Λ| < 2·B^{-C}
|
||
| C -- marginal: |Λ| ≈ B^{-C}
|
||
| B -- collision: Λ = 0 exactly
|
||
| S -- symmetric partner of a known collision
|
||
| P -- potential violation: |Λ| < B^{-C}
|
||
| Z -- zero region: |Λ| ≈ 0 but no integer lattice point
|
||
deriving DecidableEq, Repr, Fintype
|
||
|
||
/-- There are exactly 8 Hachimoji bases. -/
|
||
theorem HachimojiBase.card_eq : Fintype.card HachimojiBase = 8 := by
|
||
rw [Fintype.card_ofFinset]
|
||
· simp [HachimojiBase.A, HachimojiBase.T, HachimojiBase.G, HachimojiBase.C,
|
||
HachimojiBase.B, HachimojiBase.S, HachimojiBase.P, HachimojiBase.Z]
|
||
rfl
|
||
· intro x
|
||
simp
|
||
|
||
/-- The Hachimoji states as a type with 8 elements. -/
|
||
def HachimojiState := Fin 8
|
||
|
||
/-- Bijection between HachimojiBase and Fin 8. -/
|
||
def hachimojiToFin : HachimojiBase ≃ Fin 8 where
|
||
toFun
|
||
| .A => 0 | .T => 1 | .G => 2 | .C => 3
|
||
| .B => 4 | .S => 5 | .P => 6 | .Z => 7
|
||
invFun i := match i.val with
|
||
| 0 => .A | 1 => .T | 2 => .G | 3 => .C
|
||
| 4 => .B | 5 => .S | 6 => .P | _ => .Z
|
||
left_inv x := by cases x <;> rfl
|
||
right_inv i := by fin_cases i <;> rfl
|
||
|
||
/-- The probability simplex over 8 Hachimoji states: Δ⁷. -/
|
||
def HachimojiSimplex := openSimplex 8
|
||
|
||
/-- The Fisher metric on the Hachimoji simplex. -/
|
||
noncomputable def hachimojiFisherMetric (p : HachimojiSimplex) (X Y : Fin 8 → ℝ) : ℝ :=
|
||
fisherMetric p X Y
|
||
|
||
/-- **Chentsov's Theorem for n=8 (Hachimoji).**
|
||
The Fisher metric is the unique Chentsov-invariant metric.
|
||
The 8-state structure FORCES this metric. -/
|
||
theorem chentsov_hachimoji (g : RiemannianMetric 8)
|
||
(h_inv : IsChentsovInvariant g)
|
||
(h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex 8 =>
|
||
g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) :
|
||
∃ (c : ℝ), c > 0 ∧ ∀ (p : HachimojiSimplex) (X Y : Fin 8 → ℝ),
|
||
(∑ i, X i = 0) → (∑ i, Y i = 0) →
|
||
g.toFun p X Y = c * hachimojiFisherMetric p X Y := by
|
||
have h_n : 8 ≥ 3 := by norm_num
|
||
rcases chentsov_theorem 8 h_n g h_inv h_smooth with ⟨c, hc_pos, h_eq⟩
|
||
use c, hc_pos
|
||
exact h_eq
|
||
|
||
end HachimojiConnection
|
||
|
||
|
||
-- ============================================================
|
||
-- §9 THE MANIFOLD AXIOM IS CANONICAL
|
||
-- ============================================================
|
||
|
||
section ManifoldAxiomCanonical
|
||
|
||
/-- The 8 Hachimoji states as Greek letters (Φ Λ Ρ Κ Ω Σ Π Ζ). -/
|
||
inductive GreekHachimoji where
|
||
| Φ -- phi: trivial regime
|
||
| Λ -- lam: room regime
|
||
| Ρ -- rho: tight regime
|
||
| Κ -- kap: marginal regime
|
||
| Ω -- ome: collision state
|
||
| Σ -- sig: symmetric partner
|
||
| Π -- pi: potential violation
|
||
| Ζ -- zet: zero region
|
||
deriving DecidableEq, Repr, Fintype
|
||
|
||
/-- Bijection between Greek and Latin encodings. -/
|
||
def greekToLatin : GreekHachimoji ≃ HachimojiBase where
|
||
toFun
|
||
| .Φ => .A | .Λ => .T | .Ρ => .G | .Κ => .C
|
||
| .Ω => .B | .Σ => .S | .Π => .P | .Ζ => .Z
|
||
invFun
|
||
| .A => .Φ | .T => .Λ | .G => .R | .C => .K
|
||
| .B => .Ω | .S => .Σ | .P => .Π | .Z => .Z
|
||
left_inv x := by cases x <;> rfl
|
||
right_inv x := by cases x <;> rfl
|
||
|
||
/-- **Corollary: The Hachimoji metric is canonical.**
|
||
Chentsov's theorem forces the Fisher metric on Δ⁷.
|
||
The geometric structure is uniquely determined. -/
|
||
theorem hachimoji_metric_is_canonical (g : RiemannianMetric 8)
|
||
(h_inv : IsChentsovInvariant g)
|
||
(h_smooth : ∀ i j, ContinuousOn (fun p : openSimplex 8 =>
|
||
g.toFun p (tangentBasis i 0) (tangentBasis j 0)) (Set.univ)) :
|
||
∃ (c : ℝ), c > 0 ∧
|
||
∀ (p : openSimplex 8) (X Y : Fin 8 → ℝ),
|
||
(∑ i, X i = 0) → (∑ i, Y i = 0) →
|
||
g.toFun p X Y = c * fisherMetric p X Y := by
|
||
rcases chentsov_hachimoji g h_inv h_smooth with ⟨c, hc_pos, h_eq⟩
|
||
use c, hc_pos
|
||
exact h_eq
|
||
|
||
end ManifoldAxiomCanonical
|