SilverSight/TRACEABILITY_GRAPH.md

TRACEABILITY GRAPH

Every formula has a pedigree. Trace it back to verified basics.

Rule: A formula is only as strong as its weakest dependency. If any node in the chain is a SORRY, everything downstream stops.

---

THE FOUNDATION (given — established mathematics)

[F0] √a · √b = √(a·b)          GIVEN   (field property of ℝ≥₀)
[F1] Chentsov's theorem (1972)   PARTIAL — see LEAN FORMALIZATION below
[F2] S⁷ round metric             GIVEN   (standard Riemannian geometry)
[F3] arccos: [-1,1] → [0,π]     GIVEN   (standard calculus)

Status: GIVEN — these are not proven here. They are established results. [F1] has been partially formalized in Lean 4 (invariance leg proven, uniqueness axiomatized with citations to Chentsov 1982). See LEAN FORMALIZATION section below. If any GIVEN is ever falsified, the entire graph collapses.

---

LEAN FORMALIZATION — ChentsovFinite.lean

File: formal/CoreFormalism/ChentsovFinite.lean Classical source: N.N. Chentsov, "Statistical Decision Rules and Optimal Inference" (1982)

Formula / Concept	Declaration	Line	Status
Open probability simplex Δⁿ	openSimplex	60	✅ PROVEN
Fisher metric g_p(u,v) = Σ uᵢvᵢ/pᵢ	fisherMetric	316	✅ PROVEN
Chentsov invariance condition	IsChentsovInvariant	379	✅ PROVEN (def)
Permutation invariance condition	IsPermutationInvariant	385	✅ PROVEN (def)
Fisher metric IS Chentsov-invariant	fisher_chentsov_invariance	407	✅ PROVEN (Lean)
Metric = λ_N·Euclidean at uniform (Schur)	metric_at_uniform	694	✅ PROVEN (Lean)
λ_N/N = C (dimension-independent)	equal_refinement_const_axiom	851	AXIOM — Chentsov §12.3
g_p = C·Fisher at rational p	fisher_on_rational_axiom	884	AXIOM — Chentsov §12.4
Full uniqueness theorem	chentsov_theorem_axiom	926	AXIOM — Chentsov §12.5

Upgrade path for remaining axioms:

• Line 851: build m-way equal-split SplitEmbedding chain by induction
• Line 884: construct Markov projection kernel mapping uniform_M → rational p
• Line 926: add smoothness hypothesis to RiemannianMetric; apply rational-density lemma

---

THE CHAIN (verified in this project)

                    [F0] √a·√b = √(ab)
                           │
                           ▼
[F1] Chentsov (invariant, not unique) ──→ [V1] g_p(u,v) = Σ uᵢvᵢ/pᵢ
                           │
                           ▼
                    [V2] φ(p) = (√p₁,...,√p₈) ∈ S⁷
                           │
                           ▼
              [F0+F2] ──→ [V3] d_{S⁷}(a,b) = arccos(⟨a,b⟩)
                           │
                           ▼
              [V2+V3] ──→ [V4] ⟨φ(p),φ(q)⟩ = Σ√(pᵢqᵢ)    ← 3 AGENTS VERIFIED
                           │                                    CONSENSUS: 0.97586930
                           ▼
        [V1+V3+V4] ──→   [V5] d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ)) ← 3 AGENTS VERIFIED
                                                                CONSENSUS: 0.440258

Legend:

• [F#] = Foundation node (GIVEN, not proven here)
• [V#] = Verified node (proven + 3-agent consensus in this project)
• Arrow = logical dependency

---

VERIFIED NODES

Node	Formula	Depends On	Verified By	Consensus Value	Status
V1	g_p(u,v) = Σ uᵢvᵢ/pᵢ	F1 (Chentsov invariant)	Lean: fisherMetric (ChentsovFinite.lean:316) + fisher_chentsov_invariance (line 407, PROVEN)	N/A	✅ INVARIANT + LEAN PROVEN
V2	φ(p) = (√p₁,...,√p₈)	V1 (metric def)	Direct calc	‖φ(p)‖₂ = 1.0	✅ VERIFIED
V3	d_{S⁷}(a,b) = arccos(⟨a,b⟩)	F2 (round metric)	Given theorem	N/A	✅ GIVEN
V4	⟨φ(p),φ(q)⟩ = Σ√(pᵢqᵢ)	V2 + F0	Alpha,Beta,Gamma	0.97586930	✅ 3-AGENT
V5	d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ))	V1+V3+V4	Alpha,Beta,Gamma	0.440258	✅ 3-AGENT

---

DOWNSTREAM (pending verification)

These formulas depend on V5 being correct. They cannot be verified until V5 is firm, and they each need their own 3-agent verification.

[V5] d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ))
        │
        ├──→ [P1] C(p) = ((p₁+p₂)/2, (p₁+p₂)/2, ..., (p₇+p₈)/2)
        │           Status: PENDING — needs 3-agent verification
        │           Test: Apply C to test vector, check output sums to 1
        │
        ├──→ [P2] C(C(p)) = C(p)  (idempotence)
        │           Status: PENDING — needs 3-agent verification
        │           Depends on: P1
        │
        ├──→ [P3] d_F(C(p),C(q)) ≤ d_F(p,q)  (contraction)
        │           Status: PENDING — needs 3-agent verification
        │           Depends on: P1 + V5
        │
        ├──→ [P4] I_loss(p) = Σₖ sₖ·KL(p_{2k-1}/sₖ ‖ ½)
        │           Status: PENDING — needs 3-agent verification
        │           Depends on: P1 + V5
        │
        └──→ [P5] Φ-corkscrew: f(n) = (√n·cos(nψ), √n·sin(nψ))
                    Status: PENDING — needs 3-agent verification
                    Depends on: V5 (for the S⁷ embedding context)

Rule: P1 through P5 are SORRIES until 3-agent verified. No code for them.

---

THE TRACEABILITY TEST

For any claimed result, ask: Trace it back. What's the oldest verified node?

Example — d_F(p,q) = 0.440258:

d_F(p,q) = 0.440258
    ← V5: d_F(p,q) = 2·arccos(Σ√(pᵢqᵢ))
        ← V4: ⟨φ(p),φ(q)⟩ = Σ√(pᵢqᵢ) = 0.97586930
            ← V2: φ(p) = (√p₁,...,√p₈)
                ← V1: g_p(u,v) = Σ uᵢvᵢ/pᵢ
                    ← F1: Chentsov's theorem (1972)
            ← F0: √a·√b = √(ab)
        ← V3: d_{S⁷} = arccos(⟨a,b⟩)
            ← F2: S⁷ round metric

If you doubt 0.440258, trace it. The weakest link is F1 (Chentsov's theorem, given, not proven here) or F0 (field property, given). If you accept those, the number follows inevitably.

---

WHAT TRACING BUYS US

1. No hand-waving: Every formula has a paper trail.
2. Targeted re-verification: If a node is questioned, only that node and downstream nodes need re-checking. Upstream verified nodes stand.
3. Clear SORRY boundaries: If P3 (contraction) fails, we know P1 and V5 are still solid. The failure is isolated to the contraction claim.
4. Independent audit: An outsider can verify any node independently by tracing back to F0-F3.

---

CURRENT PROJECT STATUS

GIVEN:    F0, F2, F3              (3 foundation nodes — F1 now PARTIAL)
LEAN:     F1 (partial)            formal/CoreFormalism/ChentsovFinite.lean
           ├── PROVEN: fisherMetric (line 316), IsChentsovInvariant (line 379)
           ├── PROVEN: fisher_chentsov_invariance (line 407)
           ├── PROVEN: metric_at_uniform / Schur (line 694)
           └── AXIOM:  uniqueness chain (lines 851, 884, 926) — Chentsov §12.3-12.5
VERIFIED: V1, V2, V3, V4, V5     (5 verified nodes, 2 with 3-agent consensus)
           V1 now backed by Lean proof (ChentsovFinite.lean:407)
PENDING:  P1, P2, P3, P4, P5     (5 formulas awaiting 3-agent verification)
SORRY:    S1-S10                  (10 items from adversarial review awaiting resolution)

Next action: 3-agent verification of P1 (pair-averaging map C(p)). Lean next: close axioms at lines 851/884/926 — equal-split chain + Markov projection kernel.