mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
0b472972c2
- SDPVerify.lean: certificate verification engine (714 lines, compiles cleanly) - GoormaghtighCert.lean: Goormaghtigh conjecture SDP certificate - HachimojiManifoldAxiom/HachimojiSubstitution: Hachimoji DNA encoding - GeneticBraidBridge.lean: genetic algorithm braid bridge - load_dependency_graph/load_module_graph: Gremlin Cosmos DB graph loaders - test_graph_queries/rrc_math_xref: graph verification queries - Gremlin mathblob DB provisioned and accessible - Branch cleanup: deleted 11 stale remote branches Build: 3297 jobs, 0 errors (lake build Semantics.SDPVerify)
63 lines
2.3 KiB
Python
63 lines
2.3 KiB
Python
#!/usr/bin/env -S uv run
|
|
# /// script
|
|
# requires-python = ">=3.11"
|
|
# dependencies = ["gremlinpython", "python-dotenv"]
|
|
# ///
|
|
import os
|
|
from pathlib import Path
|
|
from dotenv import load_dotenv
|
|
load_dotenv(Path(__file__).parent.parent / ".env.gremlin")
|
|
from gremlin_python.driver import client as gc, serializer
|
|
|
|
c = gc.Client(os.environ["GREMLIN_ENDPOINT"], "g",
|
|
username=os.environ["GREMLIN_USERNAME"],
|
|
password=os.environ["GREMLIN_PASSWORD"],
|
|
message_serializer=serializer.GraphSONSerializersV2d0())
|
|
|
|
def q(query, b=None):
|
|
return c.submitAsync(query, b or {}).result().all().result()
|
|
|
|
print("═"*60)
|
|
print("Q1: Braid modules with sorries")
|
|
print("─"*60)
|
|
r = q("g.V().hasLabel('module').has('math_kind','braid').has('sorry_count',gt(0))"
|
|
".project('module','sorries','theorems')"
|
|
".by('id').by('sorry_count').by('theorem_count')")
|
|
for row in r:
|
|
print(f" {row['module'].split('.')[-1]:40s} sorry={row['sorries']} thm={row['theorems']}")
|
|
|
|
print()
|
|
print("═"*60)
|
|
print("Q2: Number_theory modules imported by quantum modules")
|
|
print("─"*60)
|
|
r = q("g.V().hasLabel('module').has('math_kind','quantum')"
|
|
".out('imports').has('math_kind','number_theory').dedup()"
|
|
".project('module','sorries','theorems')"
|
|
".by('id').by('sorry_count').by('theorem_count')")
|
|
for row in r:
|
|
print(f" {row['module'].split('.')[-1]:40s} sorry={row.get('sorries','?')} thm={row.get('theorems','?')}")
|
|
|
|
print()
|
|
print("═"*60)
|
|
print("Q3: Top theorem-producing modules per math_kind")
|
|
print("─"*60)
|
|
for kind in ["braid","number_theory","quantum","geometry","algebra"]:
|
|
r = q("g.V().hasLabel('module').has('math_kind',mk)"
|
|
".order().by('theorem_count',decr).limit(3)"
|
|
".project('m','t').by('id').by('theorem_count')",
|
|
{"mk": kind})
|
|
tops = ", ".join(f"{x['m'].split('.')[-1]}({x['t']})" for x in r)
|
|
print(f" {kind:15s}: {tops}")
|
|
|
|
print()
|
|
print("═"*60)
|
|
print("Q4: Modules with both high theorem count AND sorries")
|
|
print("─"*60)
|
|
r = q("g.V().hasLabel('module').has('theorem_count',gt(5)).has('sorry_count',gt(0))"
|
|
".order().by('sorry_count',decr)"
|
|
".project('m','s','t','k')"
|
|
".by('id').by('sorry_count').by('theorem_count').by('math_kind')")
|
|
for row in r:
|
|
print(f" {row['m'].split('.')[-1]:40s} sorry={row['s']} thm={row['t']} [{row['k']}]")
|
|
|
|
c.close()
|