mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
Lean proof fixes: - N3L_Energy.lean: fully close gaussian_line_integral_unit_dir (nlinarith+hab for unit-circle quadratic, sqrt_mul+neg_div for integral_gaussian_1d match, exp_sum_of_sq order fix, add_assoc for h_gauss_shift, sq_sqrt for field_simp, sq_abs for perpDistance hd) - Add Adapters/AlphaProofNexus: 12 Erdos/graph adapter stubs (AlphaProof nexus) - Add Adapters/ErgodicAdditive.lean, SidonMatroid.lean - Add AntiDiophantine.lean, EffectiveBoundDQ.lean, PVGS_DQ_Bridge.lean - Add FormalConjectures/Util/ProblemImports.lean - Add RRC/EntropyCandidates/Candidates.lean - Add OTOM external project (lakefile.toml, lake-manifest.json, lean-toolchain) Infrastructure: - Add 4-Infrastructure/shim/: 17 Python probes (RRC manifold, Sidon kernel, Wannier, arxiv harvest, math_symbols DB, coverage density, geometric entropy) - Add 4-Infrastructure/NoDupeLabs/: Node server + package files - Add 6-Documentation/docs/specs/DP_RRC_RECEIPT_ENCODING_SPEC.md - Add fix_offloat.py Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
213 lines
6.8 KiB
Python
213 lines
6.8 KiB
Python
#!/usr/bin/env python3
|
||
"""
|
||
build_math_symbols_db.py — Build a full math-symbol database for the RRC kernels.
|
||
|
||
Fuses two authoritative sources into one local JSON table:
|
||
|
||
1. unicode-math-table.tex (wspr/unicode-math, ~3600 entries) — the canonical
|
||
Unicode ↔ LaTeX-command ↔ math-class ↔ name mapping.
|
||
2. Python stdlib `unicodedata` — category + offline completeness
|
||
for every math symbol (category Sm) plus the Greek, Letterlike and
|
||
Mathematical-Alphanumeric blocks.
|
||
|
||
Output: shared-data/data/math_symbols_v1.json
|
||
{ "generated": "...", "count": N, "source": "...",
|
||
"symbols": [ {cp, char, name, category, block, role, latex}, ... ] }
|
||
|
||
The DB powers `math_symbols.normalize_math()` so the geometry / tensor notation
|
||
kernel matches regardless of input encoding (\\Gamma ≡ Γ, \\rho\\sigma ≡ ρσ, …).
|
||
|
||
Usage:
|
||
python3 4-Infrastructure/shim/build_math_symbols_db.py
|
||
"""
|
||
from __future__ import annotations
|
||
|
||
import json
|
||
import re
|
||
import sys
|
||
import time
|
||
import unicodedata
|
||
from pathlib import Path
|
||
|
||
ROOT = Path("/home/allaun/Research Stack")
|
||
TABLE_TEX = ROOT / "shared-data/data/unicode-math-table.tex"
|
||
OUT = ROOT / "shared-data/data/math_symbols_v1.json"
|
||
|
||
# Major math-relevant Unicode blocks (name, lo, hi) — used for `block` + offline
|
||
# completeness when a codepoint is absent from unicode-math-table.tex.
|
||
BLOCKS = [
|
||
("Basic Latin", 0x0021, 0x007E),
|
||
("Greek and Coptic", 0x0370, 0x03FF),
|
||
("Letterlike Symbols", 0x2100, 0x214F),
|
||
("Arrows", 0x2190, 0x21FF),
|
||
("Mathematical Operators", 0x2200, 0x22FF),
|
||
("Miscellaneous Technical", 0x2300, 0x23FF),
|
||
("Miscellaneous Mathematical Symbols-A", 0x27C0, 0x27EF),
|
||
("Supplemental Arrows-A", 0x27F0, 0x27FF),
|
||
("Supplemental Arrows-B", 0x2900, 0x297F),
|
||
("Miscellaneous Mathematical Symbols-B", 0x2980, 0x29FF),
|
||
("Supplemental Mathematical Operators", 0x2A00, 0x2AFF),
|
||
("Mathematical Alphanumeric Symbols", 0x1D400, 0x1D7FF),
|
||
("Arabic Mathematical Alphabetic Symbols", 0x1EE00, 0x1EEFF),
|
||
]
|
||
|
||
|
||
def block_of(cp: int) -> str:
|
||
for name, lo, hi in BLOCKS:
|
||
if lo <= cp <= hi:
|
||
return name
|
||
return "Other"
|
||
|
||
|
||
# math-class (from the .tex) → coarse structural role used by the kernels.
|
||
CLASS_ROLE = {
|
||
"mathalpha": "letter",
|
||
"mathbin": "binary_op",
|
||
"mathrel": "relation",
|
||
"mathop": "operator",
|
||
"mathord": "ordinary",
|
||
"mathopen": "delimiter_open",
|
||
"mathclose": "delimiter_close",
|
||
"mathfence": "delimiter",
|
||
"mathpunct": "punctuation",
|
||
"mathaccent": "accent",
|
||
"mathbotaccent": "accent",
|
||
"mathover": "accent",
|
||
"mathunder": "accent",
|
||
}
|
||
|
||
_NARY_HINT = ("N-ARY", "INTEGRAL", "SUMMATION", "PRODUCT", "CONTOUR",
|
||
"COPRODUCT", "BIG ", "UNION", "INTERSECTION")
|
||
|
||
|
||
def refine_role(role: str, cp: int, name: str) -> str:
|
||
up = name.upper()
|
||
if role == "operator" and any(h in up for h in _NARY_HINT):
|
||
return "nary_operator"
|
||
if role == "letter":
|
||
if 0x0370 <= cp <= 0x03FF:
|
||
return "greek_letter"
|
||
if 0x1D400 <= cp <= 0x1D7FF:
|
||
return "math_letter"
|
||
if 0x2190 <= cp <= 0x21FF or 0x27F0 <= cp <= 0x297F:
|
||
if role in ("relation", "ordinary", "symbol"):
|
||
return "arrow"
|
||
return role
|
||
|
||
|
||
def parse_brace_groups(s: str, start: int, n: int) -> list[str] | None:
|
||
"""Extract the next `n` balanced {...} groups from s starting at `start`."""
|
||
groups, i, L = [], start, len(s)
|
||
for _ in range(n):
|
||
while i < L and s[i] != "{":
|
||
i += 1
|
||
if i >= L:
|
||
return None
|
||
depth, j = 0, i
|
||
while j < L:
|
||
if s[j] == "{":
|
||
depth += 1
|
||
elif s[j] == "}":
|
||
depth -= 1
|
||
if depth == 0:
|
||
break
|
||
j += 1
|
||
groups.append(s[i + 1:j])
|
||
i = j + 1
|
||
return groups
|
||
|
||
|
||
def parse_table_tex(path: Path) -> dict[int, dict]:
|
||
"""Parse unicode-math-table.tex → {codepoint: {latex, mathclass, name}}."""
|
||
out: dict[int, dict] = {}
|
||
if not path.exists():
|
||
return out
|
||
for line in path.read_text(encoding="utf-8", errors="replace").splitlines():
|
||
if not line.startswith("\\UnicodeMathSymbol"):
|
||
continue
|
||
idx = line.find("{")
|
||
groups = parse_brace_groups(line, idx, 4)
|
||
if not groups or len(groups) < 4:
|
||
continue
|
||
cp_field, cmd, mclass, desc = groups
|
||
m = re.search(r"[0-9A-Fa-f]{4,6}", cp_field)
|
||
if not m:
|
||
continue
|
||
cp = int(m.group(0), 16)
|
||
out[cp] = {
|
||
"latex": cmd.strip(),
|
||
"mathclass": mclass.strip().lstrip("\\"),
|
||
"name": desc.strip(),
|
||
}
|
||
return out
|
||
|
||
|
||
def main() -> None:
|
||
tex = parse_table_tex(TABLE_TEX)
|
||
print(f"unicode-math-table.tex entries: {len(tex)}", file=sys.stderr)
|
||
|
||
symbols: list[dict] = []
|
||
seen: set[int] = set()
|
||
|
||
def emit(cp: int) -> None:
|
||
if cp in seen:
|
||
return
|
||
ch = chr(cp)
|
||
try:
|
||
cat = unicodedata.category(ch)
|
||
uname = unicodedata.name(ch, "")
|
||
except Exception:
|
||
cat, uname = "", ""
|
||
t = tex.get(cp)
|
||
name = (t["name"] if t else uname) or uname
|
||
if not name:
|
||
return
|
||
role = CLASS_ROLE.get(t["mathclass"], "symbol") if t else "symbol"
|
||
role = refine_role(role, cp, name)
|
||
symbols.append({
|
||
"cp": f"U+{cp:04X}",
|
||
"char": ch,
|
||
"name": name,
|
||
"category": cat,
|
||
"block": block_of(cp),
|
||
"role": role,
|
||
"latex": (t["latex"] if t else ""),
|
||
})
|
||
seen.add(cp)
|
||
|
||
# 1. every entry from the authoritative LaTeX table
|
||
for cp in sorted(tex):
|
||
emit(cp)
|
||
# 2. offline completeness: all category-Sm symbols + key math blocks
|
||
for cp in range(0x110000):
|
||
ch = chr(cp)
|
||
try:
|
||
cat = unicodedata.category(ch)
|
||
except Exception:
|
||
continue
|
||
if cat == "Sm" or (block_of(cp) != "Other" and cat[0] in ("L", "S")):
|
||
emit(cp)
|
||
|
||
by_role: dict[str, int] = {}
|
||
n_latex = 0
|
||
for s in symbols:
|
||
by_role[s["role"]] = by_role.get(s["role"], 0) + 1
|
||
if s["latex"]:
|
||
n_latex += 1
|
||
|
||
OUT.parent.mkdir(parents=True, exist_ok=True)
|
||
OUT.write_text(json.dumps({
|
||
"generated": time.strftime("%Y-%m-%dT%H:%M:%SZ"),
|
||
"count": len(symbols),
|
||
"with_latex": n_latex,
|
||
"source": "unicode-math-table.tex (wspr/unicode-math) + python unicodedata",
|
||
"roles": by_role,
|
||
"symbols": symbols,
|
||
}, ensure_ascii=False, indent=1), encoding="utf-8")
|
||
|
||
print(f"Wrote {len(symbols)} symbols ({n_latex} with LaTeX) → {OUT}", file=sys.stderr)
|
||
print("Roles: " + ", ".join(f"{k}={v}" for k, v in sorted(by_role.items(), key=lambda x: -x[1])), file=sys.stderr)
|
||
|
||
|
||
if __name__ == "__main__":
|
||
main()
|