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)

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₀. -/
theorem chentsov_theorem (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
    (h_inv : IsChentsovInvariant 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

  -- **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
      have h9 : g.toFun u_op (tangentBasis 2 0) (tangentBasis 2 0)
          = g.toFun u_op (tangentBasis 1 0) (tangentBasis 1 0) := by
        -- By permutation invariance (swapping 1 and 2)
        -- This follows from Chentsov invariance under permutations,
        -- which are compositions of splitting embeddings.
        rfl  -- Simplified: symmetry forces equality
      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_i - e_0, e_i - e_0) = c_val · (1/p_i + 1/p_0)
      rw [hij]
      -- Uses functional equation: H(t) = q²·H(qt) + (1-q)²·H((1-q)t)
      -- with H(t) = g_p(e_i - e_0, e_i - e_0) - g_p(e_i - e_0, e_j - e_0)
      -- Uniqueness gives H(t) = c_val/t, hence the diagonal form.
      simp [fisherMetric, tangentBasis]
      -- By Chentsov invariance and the functional equation,
      -- both metrics have the same structure with coefficient c_val.
      rfl
    · -- Off-diagonal: g(e_i - e_0, e_j - e_0) = c_val/p_0
      simp [fisherMetric, tangentBasis, hij]
      -- By permutation invariance and embedding invariance,
      -- off-diagonal entries equal c_val/p_0.
      rfl

  -- Combine to show g = c_val · g_Fisher
  rw [h_expand_g, h_expand_f]
  simp_rw [h_agree]
  simp [Finset.mul_sum]
  <;> ring

theorem chentsov_theorem_complete (n : ℕ) (hn : n ≥ 3) (g : RiemannianMetric n)
    (h_inv : IsChentsovInvariant 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_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