SilverSight/docs/fundamental_math/PURE_FORMULA_DERIVATION.md
allaun 1794299a6c chore(quality): native_decide migration, docs, and phi pipeline cleanup
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)
2026-06-27 01:56:54 -05:00

4.8 KiB
Raw Blame History

PURE MATH FORMULA: Fisher Distance on Δ₇

Zero English inside formulas. Each equality justified. Verifiable numerically.


Domain note: All Fisher metric computations require p_i > 0 for all i. Raw byte frequencies produce p_i = 0 for 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_7 and 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

  1. Chentsov's theorem says: any metric respecting sufficient statistics MUST be the Fisher metric (up to constant).

  2. The √p embedding maps Δ₇ → S⁷ isometrically (up to factor 4).

  3. Geodesics on S⁷ are great circles with known distance formula.

  4. 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.