Systematic native_decide → dec_trivial/rfl migration across all Lean modules to comply with AGENTS.md rule 5 (no native_decide unless only option): - CoreFormalism: BraidEigensolid, BraidField, ChentsovFinite, HachimojiBase, HachimojiBridging, HachimojiCodec, HachimojiLUT, HachimojiManifoldAxiom, Q16_16Numerics - BindingSite: BindingSiteCodec, BindingSiteEntropy, BindingSiteHachimoji - SilverSight: ProductSchema, ProductWireFormat, PolyFactorIdentity, Schema, WireFormat - PVGS_DQ_Bridge: all three files (native_decide->dec_trivial) - UniversalEncoding/ChiralitySpace Additional changes: - gemma4_mcp.py: upgraded to two-tier routing (local Gemma4 + FreeLLMAPI proxy) - ChentsovFinite: added traceability map and Chentsov (1972) citation - HachimojiBase: renamed Σ→Sig, Π→Pi to avoid non-ASCII issues - Import path fixes for Mathlib 4.30.0-rc2 compatibility - Doc updates: PURE_FORMULAS, SOS_CERTIFICATE, fundamental math derivations - Build log: 2026-06-26 session findings - BRKGLASS_NR_BRACKET_PROPOSAL: updated to REAL-DATA VALIDATED status - New docs: FOUNDATIONAL_GUIDANCE, PURE_EQUATION_MAP, CHENTSOV_FINITE_MATH, BREAKGLASS_FUSION_REVIEW_SPEC, COLD_REVIEWER_FORMULA - New python: phi pipeline (equation_dna_encoder, ast_parse, charclass, consistency, embed, output), nr_bracket_validation with receipt Build: lake build SilverSightRRC — passes on all committed modules. Excluded: HachimojiN8Bridge, HachimojiCharClass (missing CoreFormalism.HachimojiManifoldAxiom olean — WIP)
15 KiB
Finite Chentsov Theorem — Complete Standalone Mathematical Derivation
Self-contained. No code, no project identifiers, no external links required. Anyone can reconstruct every formula from the definitions here.
Classical source: N. N. Chentsov, Statistical Decision Rules and Optimal Inference (Nauka, 1972; AMS Translation, 1982), Chapter 12.
PROOF STATUS KEY
| Label | Meaning |
|---|---|
| PROVEN | Argument closes by explicit calculation. Checkable line-by-line. No external citations needed. |
| PROVEN (Schur) | Closes using Schur's lemma; full self-contained proof given in Appendix A. |
| REQUIRES | Correct in intent but depends on additional structure not yet explicit. What is missing is stated precisely. |
The value of any formal verification of this theorem depends entirely on the PROVEN steps being actually proven. REQUIRES steps hold up the full uniqueness claim. Do not treat them as established until the missing structure is made explicit.
Part I — Definitions
1. The Open Probability Simplex
For n ≥ 1, the open probability simplex is:
Δₙ := { p : {0,...,n−1} → ℝ | pᵢ > 0 for all i, and Σᵢ pᵢ = 1 }
The tangent space at p ∈ Δₙ is the hyperplane of zero-sum vectors:
TₚΔₙ := { X : {0,...,n−1} → ℝ | Σᵢ Xᵢ = 0 }
The tangent basis vectors (for i ≠ j) are:
bᵢⱼ(k) := [k = i] − [k = j]
where [·] is the Iverson bracket. One verifies Σₖ bᵢⱼ(k) = 0, so bᵢⱼ ∈ TₚΔₙ for any p.
2. Markov Split Embeddings
A split embedding on Δₙ is a pair (i₀, q) where:
- i₀ ∈ {0,...,n−1} (the index to split)
- q ∈ (0,1) (the split weight)
Push-forward on distributions. Define apply(i₀, q) : Δₙ → Δₙ₊₁ by:
apply(i₀, q, p)(j) :=
q · p(i₀) if j = i₀
(1−q) · p(i₀) if j = i₀ + 1
p(j) if j < i₀
p(j − 1) if j > i₀ + 1
Verification that apply(i₀, q, p) ∈ Δₙ₊₁:
- Positivity: q · p(i₀) > 0 and (1−q) · p(i₀) > 0 since q ∈ (0,1) and p(i₀) > 0.
- Sum: q·p(i₀) + (1−q)·p(i₀) + Σⱼ≠i₀ p(j) = p(i₀) + (1 − p(i₀)) = 1. ✓
Push-forward on tangent vectors. For X ∈ TₚΔₙ define pushforward(i₀, q, X) ∈ T_{apply(p)}Δₙ₊₁ by:
pushforward(i₀, q, X)(j) :=
q · X(i₀) if j = i₀
(1−q) · X(i₀) if j = i₀ + 1
X(j) if j < i₀
X(j − 1) if j > i₀ + 1
Lemma (zero-sum preserved).
Σⱼ pushforward(i₀, q, X)(j)
= q·X(i₀) + (1−q)·X(i₀) + Σⱼ≠i₀ X(j)
= X(i₀) + Σⱼ≠i₀ X(j)
= Σⱼ X(j) = 0. ✓
3. Fisher Information Metric
For p ∈ Δₙ and X, Y ∈ TₚΔₙ define:
g^F_p(X, Y) := Σᵢ Xᵢ Yᵢ / pᵢ
Symmetry: g^F_p(X,Y) = g^F_p(Y,X) by commutativity of multiplication.
Positive definiteness: g^F_p(X,X) = Σᵢ Xᵢ²/pᵢ. Each term ≥ 0 since pᵢ > 0; the sum equals 0 iff every Xᵢ = 0. ✓
Bilinearity: immediate from linearity of summation.
4. Riemannian Metrics on Δₙ
A Riemannian metric on Δₙ is a collection
g = { g_p : TₚΔₙ × TₚΔₙ → ℝ }_{p ∈ Δₙ}
satisfying, for every p ∈ Δₙ:
- Symmetry: g_p(X,Y) = g_p(Y,X) for all X, Y.
- Bilinearity: g_p(αX+βZ, Y) = α·g_p(X,Y) + β·g_p(Z,Y) for all α,β ∈ ℝ.
- Positive definiteness: g_p(X,X) > 0 for all X ∈ TₚΔₙ \ {0}.
- Smoothness in p: the map p ↦ g_p(X,Y) is C∞ on Δₙ for each fixed X, Y.
A Chentsov-compatible family is a sequence g = {g_n}_{n≥1} where each g_n is a Riemannian metric on Δₙ, and for every n ≥ 1 and every split (i₀, q):
g_n(p)(X, Y) = g_{n+1}(apply(i₀,q,p))(pushforward(i₀,q,X), pushforward(i₀,q,Y))
for all p ∈ Δₙ, X, Y ∈ TₚΔₙ. (This is what §5 verifies for g^F.)
A family is permutation-invariant if for every n ≥ 1, every permutation σ : {0,...,n−1} → {0,...,n−1}, and every p ∈ Δₙ:
g_n(p)(X, Y) = g_n(p∘σ⁻¹)(X∘σ⁻¹, Y∘σ⁻¹)
Part II — The Invariance Theorem (PROVEN)
5. The Fisher Metric is Chentsov-Compatible (PROVEN)
Theorem. g^F forms a Chentsov-compatible family. That is, for every n ≥ 1, every split (i₀, q), every p ∈ Δₙ, and all X, Y ∈ TₚΔₙ with Σᵢ Xᵢ = Σᵢ Yᵢ = 0:
g^F_p(X, Y) = g^F_{apply(p)}(pushforward(X), pushforward(Y))
Proof. Write i = i₀. Let p' = apply(i,q,p), X' = pushforward(i,q,X), Y' = pushforward(i,q,Y). Split {0,...,n} into three parts:
(A) j = i: X'(i) = q·X(i), Y'(i) = q·Y(i), p'(i) = q·p(i) → X'(i)·Y'(i)/p'(i) = q²·X(i)Y(i) / (q·p(i)) = q · X(i)Y(i)/p(i)
(B) j = i+1: X'(i+1) = (1−q)·X(i), Y'(i+1) = (1−q)·Y(i), p'(i+1) = (1−q)·p(i) → X'(i+1)·Y'(i+1)/p'(i+1) = (1−q) · X(i)Y(i)/p(i)
(C) j ∉ {i, i+1}: X'(j) = X(j−δ), Y'(j) = Y(j−δ), p'(j) = p(j−δ) where δ = 1 if j > i+1, else 0. → contribution X(j−δ)·Y(j−δ)/p(j−δ) = X(k)·Y(k)/p(k) for k = j−δ ≠ i. Together (C) = Σₖ≠ᵢ X(k)Y(k)/p(k).
Summing (A)+(B)+(C):
g^F_{p'}(X', Y')
= q·X(i)Y(i)/p(i) + (1−q)·X(i)Y(i)/p(i) + Σₖ≠ᵢ X(k)Y(k)/p(k)
= X(i)Y(i)/p(i) + Σₖ≠ᵢ X(k)Y(k)/p(k)
= Σₖ X(k)Y(k)/p(k)
= g^F_p(X, Y). ∎
Part III — Uniqueness Steps
6. Metric at the Uniform Point — Schur's Lemma (PROVEN (Schur))
For n ≥ 1, the uniform distribution is uₙ = (1/n, ..., 1/n) ∈ Δₙ.
Theorem. Let g be a Riemannian metric on Δₙ (n ≥ 2) that is permutation-invariant. Then there exists λₙ > 0 such that for all X, Y ∈ T_{uₙ}Δₙ:
g_{uₙ}(X, Y) = λₙ · Σᵢ Xᵢ Yᵢ
Proof. The symmetric group Sₙ acts on V := T_{uₙ}Δₙ by (σ·X)ᵢ = X_{σ⁻¹(i)}. Permutation-invariance says g_{uₙ}(σ·X, σ·Y) = g_{uₙ}(X,Y) for all σ ∈ Sₙ. By Appendix A, V is an irreducible Sₙ-module and every Sₙ-equivariant symmetric bilinear form on V is a scalar multiple of the standard inner product ⟨X,Y⟩ = ΣXᵢYᵢ. Therefore g_{uₙ} = λₙ·⟨·,·⟩ for some λₙ ∈ ℝ. Positivity λₙ > 0 follows from g_{uₙ} being positive definite on V \ {0}. ∎
7. Dimension-Independence of Constant (PROVEN)
Setup. Let g = {gₙ}_{n≥1} be a Chentsov-compatible, permutation-invariant family. By §6, each gₙ has a scalar λₙ > 0 at the uniform point uₙ.
Theorem. There exists C > 0 such that λₙ = C · n for all n ≥ 1.
Proof.
Step 1 — m-fold equal split via binary chain. Fix n ≥ 1, m ≥ 2. We construct a chain of (n·(m−1)) binary splits that maps uₙ to u_{nm} by splitting each original state into m equal parts.
For a single state i with current weight w, the chain to split it into m equal parts of weight w/m uses m−1 binary splits in sequence:
- Split r (for r = 1,...,m−1): take the rightmost unsplit piece of state i (currently carrying weight (m−r+1)·w/m at relative position r−1), and split it with q_r = 1/(m−r+1), producing one piece of weight w/m and one remaining piece of weight (m−r)·w/m.
After all m−1 splits, state i has been divided into m positions each carrying weight w/m.
Applied to every state i = 0,...,n−1 of uₙ (each with w = 1/n), the full chain produces n·m states each of weight 1/n · 1/m = 1/(nm), which is u_{nm}.
Step 2 — Pushforward of tangent vectors: inductive calculation. We show by induction on r (number of splits applied to state i) that after r splits, the r+1 sub-pieces of state i each carry tangent-vector weight X(i)/(r+1).
Base case (r = 0): state i carries X(i) = X(i)/1. ✓
Inductive step: Suppose after r splits, the r+1 sub-pieces carry X(i)/(r+1) each. The next split has q_{r+1} = 1/(r+2) and acts on the last sub-piece (weight X(i)/(r+1)). By the pushforward definition:
- New piece: q_{r+1} · X(i)/(r+1) = X(i)/(r+2)
- Remaining: (1−q_{r+1}) · X(i)/(r+1) = (r+1)/(r+2) · X(i)/(r+1) = X(i)/(r+2)
So after r+1 splits, the r+2 sub-pieces each carry X(i)/(r+2). ✓
After m−1 splits (r = m−1), all m sub-pieces of state i carry X(i)/m.
Step 3 — Composite pushforward inner product. Let X' ∈ T_{u_{nm}}Δ_{nm} be the composite pushforward of X ∈ T_{uₙ}Δₙ. By Step 2, X'(i·m + k) = X(i)/m for each i ∈ {0,...,n−1} and k ∈ {0,...,m−1}. Therefore:
Σⱼ X'(j)·Y'(j)
= Σᵢ₌₀^{n−1} Σₖ₌₀^{m−1} (X(i)/m)·(Y(i)/m)
= Σᵢ₌₀^{n−1} m · X(i)Y(i)/m²
= (1/m) · Σᵢ X(i)Y(i)
Step 4 — Chentsov-invariance forces λ_{nm} = m · λₙ. Apply Chentsov-compatibility through the full binary chain:
gₙ(uₙ)(X, Y) = g_{nm}(u_{nm})(X', Y')
Substituting the uniform-point scalars from §6:
λₙ · Σᵢ X(i)Y(i) = λ_{nm} · (1/m) · Σᵢ X(i)Y(i)
Since ΣX(i)Y(i) can be any real number (the tangent space has dimension n−1 ≥ 1), cancel it to obtain:
λₙ = λ_{nm} / m → λ_{nm} = m · λₙ
Step 5 — C is independent of dimension. Define C := λₙ / n. For any other dimension n' = nm:
λ_{n'} / n' = λ_{nm} / (nm) = m·λₙ / (nm) = λₙ / n = C
So C is the same for every n. C > 0 follows from λₙ > 0. ∎
8. Rational Points — g = C · Fisher (REQUIRES additional structure)
Goal. For every rational p = (k₁/M, ..., k_n/M) ∈ Δₙ with kᵢ ∈ ℕ, Σkᵢ = M:
gₙ(p)(X, Y) = C · g^F_p(X, Y) for all X, Y ∈ TₚΔₙ
What the Chentsov-compatible condition gives. The definition in §4 says: for every binary split (Δₙ → Δₙ₊₁), the metric at p equals the metric at apply(p). This constrains gₙ(p) in terms of g_{n+1} at refinements of p — it says nothing directly about the metric at coarsenings.
The gap. To reach rational p from the uniform point, the natural route uses a COARSENING: take u_M and apply a stochastic map T: Δ_M → Δₙ (with M > n) that groups the M states into n blocks of sizes k₁,...,kₙ. A coarsening is the opposite direction from a split embedding. The Chentsov-compatible condition as defined does NOT constrain gₙ(p) via coarsenings.
What would close §8. Either:
(A) A direct algebraic argument showing that Chentsov-compatibility for ALL binary splits and ALL dimensions forces gₙ(p) = C·g^F_p at rational p — without needing any coarsening. This requires showing that the infinite system of equations "gₙ(p) = g_{n+1}(apply(p)) for all splits of all refinements of p" uniquely determines gₙ(p).
(B) Extending the compatibility condition to include coarsenings. Specifically, require that for every stochastic matrix T: Δ_M → Δₙ and every q ∈ Δ_M with T(q) = p: gₙ(p)(TX, TY) ≤ g_M(q)(X, Y) (information monotonicity) The equality case T(u_M) = p with T being the block-grouping map then gives §8. This is the condition used in Chentsov's original theorem.
Until (A) or (B) is completed, §8 is not derivable from the split-embedding axioms alone.
9. Full Uniqueness — Density and Smoothness (REQUIRES §8 + smoothness)
Goal. Let n ≥ 3. If g = {gₙ} is a Chentsov-compatible, permutation-invariant family that is smooth in p (per §4), then:
gₙ(p)(X, Y) = C · g^F_p(X, Y) for all p ∈ Δₙ, X, Y ∈ TₚΔₙ
What is proven assuming §8 holds. The density + continuity argument closes completely once §8 is established:
(a) §8 gives gₙ(p) = C·g^F_p for all rational p ∈ Δₙ ∩ ℚⁿ.
(b) Rational density: Δₙ ∩ ℚⁿ is dense in Δₙ. Proof: given p ∈ Δₙ and ε > 0, choose rᵢ ∈ ℚ with |rᵢ−pᵢ| < ε/(n+1) and rᵢ > 0; adjust the last coordinate to make Σrᵢ = 1 exactly while keeping all entries positive (possible for ε small enough since pₙ₋₁ > 0).
(c) Continuity: p ↦ gₙ(p)(X,Y) is continuous by the smoothness condition in §4.
(d) Two continuous functions on the connected space Δₙ that agree on a dense subset are equal. (Proof: if they differ at some p₀, by continuity they differ on an open neighborhood of p₀, which must contain a rational point — contradiction.)
What is missing.
- §8 (see above).
- The smoothness condition is stated in §4 but must be an explicit hypothesis on the family g. It is classically satisfied by any Riemannian metric on a smooth manifold. In any formal treatment, it must be stated as a premise, not assumed.
Summary Table
| Claim | Status | Closes at | Gap (if any) |
|---|---|---|---|
| Δₙ, TₚΔₙ, tangent basis defined | DEFINITION | §1 | — |
| pushforward preserves Σ Xᵢ = 0 | PROVEN | §2 | — |
| g^F is a Riemannian metric | PROVEN | §3 | — |
| Riemannian metric defined precisely | DEFINITION | §4 | — |
| Family compatibility conditions stated | DEFINITION | §4 | — |
| g^F is Chentsov-compatible | PROVEN | §5, three-case split | — |
| gₙ at uniform point = λₙ · Euclidean | PROVEN (Schur) | §6 | Schur's lemma: Appendix A |
| λₙ/n = C (dimension-free) | PROVEN | §7, inductive pushforward | — |
| gₙ(p) = C·g^F at rational p | REQUIRES | §8 | Coarsening invariance OR algebraic closure |
| gₙ(p) = C·g^F everywhere | REQUIRES | §9 (given §8) | §8 + explicit smoothness premise |
Appendix A — Schur's Lemma for Symmetric Groups (self-contained)
Setup. Let V = ker(Σ) ⊂ ℝⁿ, i.e. V = T_{uₙ}Δₙ. The symmetric group Sₙ acts on V by (σ·X)ᵢ = X_{σ⁻¹(i)}.
Claim A1 (Irreducibility). V is irreducible as an Sₙ-module for n ≥ 2.
Proof. Let W ⊆ V be a nonzero Sₙ-stable subspace. Pick nonzero w ∈ W. Since Σwᵢ = 0 and w ≠ 0, there exist indices a ≠ b with wₐ ≠ wᵦ. Apply the transposition τ = (a b) ∈ Sₙ:
w − τ·w has components:
index a: wₐ − wᵦ ≠ 0
index b: wᵦ − wₐ ≠ 0
all others: 0
So w − τ·w is a nonzero multiple of bₐᵦ = eₐ − eᵦ, hence bₐᵦ ∈ W.
For any other pair (c,d), choose σ ∈ Sₙ with σ(a)=c, σ(b)=d; then σ·bₐᵦ = bcd ∈ W. The vectors {bᵢ₀ : i = 1,...,n−1} are a basis for V (they span ker(Σ)). So W = V. ∎
Claim A2 (Schur scalar). Let B: V × V → ℝ be a symmetric bilinear form satisfying B(σ·X, σ·Y) = B(X,Y) for all σ ∈ Sₙ and X,Y ∈ V. Then B = λ·⟨·,·⟩ for some λ ∈ ℝ.
Proof. The form B defines a symmetric linear operator T_B : V → V* ≅ V by ⟨T_B X, Y⟩ = B(X,Y). Sₙ-equivariance of B means T_B commutes with every σ ∈ Sₙ (i.e., T_B is a morphism of Sₙ-modules V → V).
Since ℝ is algebraically closed over itself and V is irreducible (Claim A1), by the real version of Schur's lemma: every Sₙ-module endomorphism of V is a scalar multiple of the identity. Therefore T_B = λ·Id for some λ ∈ ℝ, giving B(X,Y) = λ·ΣXᵢYᵢ.
If B is additionally positive definite on V \ {0}, then λ > 0. ∎
Remark on real Schur's lemma. Over ℝ, Schur's lemma states that the endomorphism algebra End_{Sₙ}(V) of a real irreducible module is a division ring (ℝ, ℂ, or ℍ). For the standard representation of Sₙ (n ≥ 3), V is absolutely irreducible (remains irreducible over ℂ), so End_{Sₙ}(V) ≅ ℝ and every endomorphism is scalar. For n = 2, dim V = 1 so the conclusion is immediate. ∎