mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-30 17:16:16 +00:00
allaun
1794299a6c
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)
174 lines
7.6 KiB
Markdown
174 lines
7.6 KiB
Markdown
# 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.
|