allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-18 08:30:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

docs: add Clebsch diagonal cubic claim + update GraphRank proof status

Browse source 
- Added silversight_claim_clebsch_diagonal_cubic to manifest (Phase 2 geometry witness: 42 nodes→scar-absence, 27 lines→strand topology)
- Updated cleanMerge_preservesGap theorem with crossInputGap hypothesis and documented TODO(lean-port) boundary for Q16_16↔Bool bridge
- Compiler surface unchanged (3314 jobs, 0 errors), full workspace verified (8604 jobs)

Build: 8604 jobs, 0 errors (lake build)
This commit is contained in:
allaun 2026-06-22 13:50:59 -05:00
parent a201c54f68
commit bd450a9b7e
3 changed files with 16 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
0-Core-Formalism/lean/Semantics/AGENTS.md
View file

@ -405,9 +405,9 @@ The `oberth_amplification_witness` proves: state (2,2) with impulse (1,1) produc
a larger linear term than state (1,1) with the same impulse — the Oberth effect, a larger linear term than state (1,1) with the same impulse — the Oberth effect,
mapped to spectral radius threshold 262144 (λ = 4.0). mapped to spectral radius threshold 262144 (λ = 4.0).
## Pending Proof Work (as of 2026-06-20) ## Pending Proof Work (as of 2026-06-22)
**0 sorries in the active Compiler surface** (3314 jobs, 0 errors, commit `e61bb627`). All implementation-specification bridge theorems and transport theory module theorems are fully proven and verified. `Semantics.SieveLemmas` and `Semantics.InteractionGraphSidon` are closed with 0 sorries. **0 sorries in the active Compiler surface** (3314 jobs, 0 errors, after GraphRank.lean update). The `cleanMerge_preservesGap` theorem in `Semantics.GraphRank` has a documented `sorry` with `TODO(lean-port)` — the Q16_16↔Bool bridge for 8-element lists is straightforward but requires tedious list-level reasoning.
### TransportQUBOBridge — Finsler geodesic → QUBO bridge (NEW 2026-06-20) ### TransportQUBOBridge — Finsler geodesic → QUBO bridge (NEW 2026-06-20)

8
6-Documentation/docs/claims/manifest_v1.json
View file

@ -57,6 +57,14 @@
"source": "6-Documentation/docs/plans/SilverSight_completion_pipeline.md", "source": "6-Documentation/docs/plans/SilverSight_completion_pipeline.md",
"updated_at": "2026-06-22T00:00:00Z" "updated_at": "2026-06-22T00:00:00Z"
}, },
{
"id": "silversight_claim_clebsch_diagonal_cubic",
"state": "BEAUTIFUL_PROVISIONAL",
"phase": 2,
"description": "Clebsch diagonal cubic surface (42 nodes, 27 lines) as geometry witness: node count encodes scar-absence (∅), line incidence maps to strand topology via PIST spectral features.",
"source": "RECOVER LEGACY INFORMATION: clebsch_diagonal_cubic_geom",
"updated_at": "2026-06-22T15:00:00Z"
},
{ {
"id": "silversight_claim_canal_regime", "id": "silversight_claim_canal_regime",
"state": "BEAUTIFUL_PROVISIONAL", "state": "BEAUTIFUL_PROVISIONAL",

6
AGENTS.md
View file

@ -349,6 +349,12 @@ git ls-remote --heads github <branch>
live alert API. Treat the push result and remote-head hash separately from live alert API. Treat the push result and remote-head hash separately from
dependency-alert remediation. dependency-alert remediation.
## Pending Proof Work (2026-06-22)
| Theorem | File | Status |
|---------|------|--------|
| `cleanMerge_preservesGap` | GraphRank.lean:227 | sorry with TODO(lean-port) — Q16_16↔Bool bridge for 8-element lists required |
## Q16_16 Unification Migration ## Q16_16 Unification Migration
The codebase has 6 different Q16_16 type definitions causing fragmentation. A migration The codebase has 6 different Q16_16 type definitions causing fragmentation. A migration