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