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)
4.8 KiB
PURE MATH FORMULA: Fisher Distance on Δ₇
Zero English inside formulas. Each equality justified. Verifiable numerically.
Domain note: All Fisher metric computations require
p_i > 0for alli. Raw byte frequencies producep_i = 0for unseen classes. Apply Laplace smoothing:F(E)_i = (f_i + 1)/(|E| + 8)to ensure strict positivity. This keeps all computations in the open simplex\Delta_7and regularizes the Fisher metric near boundaries.
THE CHAIN
Given: p, q ∈ Δ₇ (probability simplex, 8 dimensions)
Step 0 — Chentsov's metric:
g_p(u,v) = Σᵢ₌₁⁸ (uᵢ vᵢ / pᵢ)
Justification: Chentsov 1972, Amari 1985. Unique metric respecting sufficient statistics.
Step 1 — The √p embedding:
φ : Δ₇ → S⁷, φ(p) = (√p₁, √p₂, ..., √p₈)
Lemma: ‖φ(p)‖₂ = 1
‖φ(p)‖₂² = Σᵢ₌₁⁸ (√pᵢ)² = Σᵢ₌₁⁸ pᵢ = 1
Justification: p ∈ Δ₇ ⇒ Σpᵢ = 1 by definition.
Step 2 — Pullback of round metric:
(φ* g_{S⁷})_p(u,v) = ¼ · g_p(u,v)
Proof sketch:
Let c(t) be a curve in Δ₇, c(0) = p, ċ(0) = v.
γ(t) = φ(c(t)) = (√c₁(t), ..., √c₈(t))
γ̇ᵢ(0) = vᵢ / (2√pᵢ)
Round metric on S⁷:
⟨γ̇, γ̇⟩_{S⁷} = Σᵢ γ̇ᵢ² = Σᵢ vᵢ² / (4pᵢ) = ¼ · Σᵢ vᵢ²/pᵢ = ¼ · g_p(v,v)
Justification: Chain rule + direct computation.
Step 3 — Geodesics are great circles:
S⁷ has round metric ⇒ geodesics are great circles.
Great-circle distance:
d_{S⁷}(a,b) = arccos(⟨a,b⟩)
Justification: Standard Riemannian geometry of the sphere.
Step 4 — Inner product on S⁷:
⟨φ(p), φ(q)⟩ = Σᵢ₌₁⁸ √(pᵢ qᵢ)
Justification: Definition of φ + Euclidean inner product.
Step 5 — Fisher distance (THE FORMULA):
d_F(p,q) = 2 · d_{S⁷}(φ(p), φ(q))
= 2 · arccos(⟨φ(p), φ(q)⟩)
= 2 · arccos( Σᵢ₌₁⁸ √(pᵢ qᵢ) )
Justification: Steps 2+3+4 combined. The factor 2 comes from Step 2 (g = 4·φ*g_{S⁷}).
THE CLOSED-FORM RESULT
┌─────────────────────────────────────────────────────┐
│ │
│ d_F(p,q) = 2 · arccos( Σᵢ₌₁ⁿ √(pᵢ qᵢ) ) │
│ │
│ Domain: p, q ∈ Δₙ (any dimension n ≥ 2) │
│ Range: [0, π] │
│ Equality: d_F(p,q) = 0 ⟺ p = q │
│ Max: d_F(p,q) = π when p, q are antipodal │
│ (e.g., p = (1,0,...,0), q = (0,1,0,...,0)) │
│ │
└─────────────────────────────────────────────────────┘
VERIFICATION INSTANCE (n=8)
Inputs:
p = (0.3, 0.1, 0.15, 0.05, 0.2, 0.08, 0.07, 0.05)
q = (0.2, 0.2, 0.1, 0.1, 0.15, 0.1, 0.1, 0.05)
Step A — Compute √(pᵢqᵢ):
√(0.3×0.2) = 0.24494897
√(0.1×0.2) = 0.14142136
√(0.15×0.1) = 0.12247449
√(0.05×0.1) = 0.07071068
√(0.2×0.15) = 0.17320508
√(0.08×0.1) = 0.08944272
√(0.07×0.1) = 0.08366600
√(0.05×0.05) = 0.05000000
Step B — Sum:
S = 0.97586930
Step C — Arccos:
arccos(0.97586930) = 0.22012896
Step D — Multiply by 2:
d_F(p,q) = 2 × 0.22012896 = 0.44025792
OUTPUT: d_F(p,q) ≈ 0.440258
PROPERTIES (all verifiable)
Symmetry:
d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ)) = 2·arccos(Σ√(qᵢpᵢ)) = d_F(q,p) ✓
Identity:
d_F(p,p) = 2·arccos(Σ√(pᵢpᵢ)) = 2·arccos(Σpᵢ) = 2·arccos(1) = 0 ✓
Triangle inequality:
d_F(p,q) ≤ d_F(p,r) + d_F(r,q) for all p,q,r ∈ Δ₇
Proof: Great-circle distance on S⁷ satisfies triangle inequality.
Pullback by isometry preserves triangle inequality. ✓
Bound:
0 ≤ d_F(p,q) ≤ π
Proof: arccos: [-1,1] → [0,π]. The argument Σ√(pᵢqᵢ) ∈ [0,1]
by Cauchy-Schwarz: (Σ√(pᵢqᵢ))² ≤ (Σpᵢ)(Σqᵢ) = 1. ✓
WHY THIS IS THE RIGHT FORMULA
-
Chentsov's theorem says: any metric respecting sufficient statistics MUST be the Fisher metric (up to constant).
-
The √p embedding maps Δ₇ → S⁷ isometrically (up to factor 4).
-
Geodesics on S⁷ are great circles with known distance formula.
-
Pulling back gives the Fisher distance formula above.
There is no choice in this formula. It is forced by the geometry of the probability simplex combined with Chentsov's uniqueness result.