diff --git a/telperion/docs/COMMENSALISM_SYNTHESIS_20260831.md b/telperion/docs/COMMENSALISM_SYNTHESIS_20260831.md new file mode 100644 index 00000000..39f2f2ab --- /dev/null +++ b/telperion/docs/COMMENSALISM_SYNTHESIS_20260831.md @@ -0,0 +1,84 @@ +# The RH–BG–(P/NP) commensalism: state of the arc (2026-08-31) + +Durable synthesis of the cross-pollination reassessment. One-line thesis: + +> **Three proof programs — the Riemann Hypothesis, Brualdi–Goldwasser, and P-vs-NP +> (SoS-3XOR) — reduce their pointwise obligations to ONE box-positivity / SOS +> certificate engine. Each program's easy *atoms* share the engine (probed green); +> each program's hard *construction* stays open in its own lane.** + +`conjecture1_proved = False` for all three. Nothing here proves, or approaches +proving, any of the three conjectures. This is shared *machinery* and honest scope. + +## Three programs, one engine + +| program | pointwise obligation | shared certificate | probe (evidence) | HARD open frontier (owned lane) | +|---|---|---|---|---| +| **RH** | ζ zero-free region `(1+x)^n ≥ 0` on `{1±x}` | Handelman box witness | `bg-handelman-shared-engine` ✓ | full zero-free region beyond the boundary; the region past R1 | +| **BG** | bulk-discharge `φ_v ≤ F*` on the field box `h∈(0,1]` | Handelman / Bernstein box-positivity | `bg-handelman-shared-engine` ✓ | the tight **field-dependent** universal `τ` | +| **P/NP** | SoS pseudo-expectation `0 ≤ pe(s²)` | exact-rational PSD moment matrix = SOS Gram | `sos_pe_probe.py` ✓ | SoS degree lower bound for UNSAT expanders | + +The engine is the same object: nonnegative combinations of box-constraint products +(Handelman) / PSD Gram (SOS) — `emit_handelman`, `emit_sos`, `emit_constrained_sos`, +`cone`, `worst_corner`. RH built and extended it (`emit_zero_free_cosine` reusing +`HandelmanEmitter`); BG and P/NP consume the same shape. + +## The arithmetic tie is BG-internal (precise) + +`621/64 = 27·23` is a **BG-internal** three-way convergence: classical-BG brooms ↔ +Φ¹¹ near-star tie (`64·243·23 = 621·576`) ↔ Lean `{4,5}` balanced-capped — all sharing +the *same* `23`. The parallel BG session proved the reconciliation exactly: +`R(s) [Φ¹¹] ≡ total(5)^(2s+1)/total(s)^11 [broom ratio]`, upgrading `c=5` to a closed +all-`c` single-crossing proof (`BG_23ADIC_RECONCILIATION_20260831.md`). + +**RH shares the ENGINE, not the 23** — there is no `23` in `(1+x)^n`. So: **two +programs (BG, Φ¹¹) meet at the 23-adic tie; all three meet at the box-positivity +engine.** (Not three-way 23-adic — the BG owner's correction, incorporated.) + +## Certificate-level reason the BG maximum sits at c=5 + +`c=5` is the UNIQUE cherry-count where the box-positivity certificate is *both* +low-degree *and* carries the exact 23-adic tie: `1+2c=11` makes `rhoB^11 = 621/64` +rational, so the 11th root cancels. For `c≠5` you get one or the other, never both — +the RH `IntervalBracket` route gives degree-3 positivity but loses the `23`; the +11th-power (`emit_padic`) route preserves `23^(1+2c)` but at degree ×11 +(`bg_c6_bracket_handelman.py`). So `emit_padic` is the tie-preserving route reserved +for `c=5`; the bracket extends the gate to all `c` for positivity only. + +## The monitor auto-discovers this + +The skill-extraction monitor (`tools/shape_scout.py`) — the mechanized +cross-pollination standing order — was run over 18,040 theorems of live work +(`MONITOR_RUN_20260831.md`). Unsupervised, it: recovered the known RH→BG channels +(`emit_padic` via `deficit_v23`, `emit_bracket` via `rhoB_sqrt2`), firewalled the 50 +tree→hub `R47R7*` obligations as STRUCTURAL (no false emit), and **surfaced the P/NP +link itself** (`Hsq:hsq_of_subsetForm` = `0 ≤ pe(s²)` → SOS). The third program +entered the picture because the monitor found it. + +## What is NOT claimed + +- No conjecture is proved or approached. `conjecture1_proved = False` throughout. +- The probed atoms are **individually easy** — feasibility/engine demonstrations, not + hard results. Each program's hard construction is open research in its own lane. +- CANDIDATE (shape-matched) ≠ certified ≠ closed. The STRUCTURAL cores (BG tree→hub, + the tight `τ`) are the real open work and no emitter reaches them. + +## Artifact index + +- **Map:** `…/laplacian_ratio/RH_EMITTER_TO_BG_OBLIGATION_MAP.md` +- **Standing order:** `telperion/docs/CROSS_POLLINATION_STANDING_ORDER.md` +- **Monitor + run:** `tools/shape_scout.py`, `docs/SKILL_EXTRACTION_MONITOR.md`, + `docs/MONITOR_RUN_20260831.md` (branch `feat/skill-extraction-monitor`) +- **Probes:** `docs/probes/bg_discharge_handelman_probe.py`, + `bg_c6_bracket_handelman.py` (branch `probe/bg-handelman-shared-engine`); + `docs/probes/sos_pe_probe.py` (this branch) +- **BG lanes:** `BG_STAR_OF_BROOMS_HANDOFF.md`, `BG_23ADIC_RECONCILIATION_20260831.md`, + `HANDOFF_TREE_TO_HUB_20260831.md`, `examples/bg_bulk_discharge` +- **Memory:** `rh-bg-shared-endgame-2026-08-31`, `telperion-cross-pollination-standing-order` + +## The compounding loop (how this arc was produced) + +A memory update seeded the BG session's Φ¹¹↔broom reconciliation → that closed the +map's bridge row and validated the Handelman probe → the probe became a kernel-gated +warm-up + narrowed the tight-`τ` crux → the monitor auto-found the P/NP link → the +SoS probe validated it. Bidirectional cross-pollination, mechanized and honest. diff --git a/telperion/docs/CROSS_POLLINATION_STANDING_ORDER.md b/telperion/docs/CROSS_POLLINATION_STANDING_ORDER.md new file mode 100644 index 00000000..b464eb74 --- /dev/null +++ b/telperion/docs/CROSS_POLLINATION_STANDING_ORDER.md @@ -0,0 +1,55 @@ +# Standing order: cross-pollinate BG ↔ RH shapes into Telperion + +**Order.** Whenever one proof effort — Brualdi–Goldwasser (BG / Laplacian) or the +Riemann Hypothesis (RH) campaign — produces a *skill or shape* in Telperion (a +new emitter kind, an `InequalityFamily` pattern, a certification discipline) that +would apply to advancing the *other* effort's goals, it MUST be done and +formalized into Telperion as a reusable capability. Cross-pollination is not +optional and not deferred to "when convenient" — a shape that helps the sister +effort is built, certified, and left in the shared emitter set. + +This generalizes the existing Telperion build standing order (build any reusable +capability that surfaces in a proof into Telperion as a skill) with an explicit +*bidirectional* obligation: RH→BG and BG→RH are first-class flows. + +## Why this is sound (the commensalism) + +Both efforts sit on one substrate: the untrusted-generator / trusted-Lean-kernel +split, exact-`Fraction` certify-before-emit, and a shared Mathlib pin under one +CI kernel gate. Their mathematics overlaps at real-rootedness / hyperbolicity +(Turán / Jensen / Hankel PSD), rational-function identities, p-adic/integrality +tie facts, SOS/Pólya positivity, and rigorous rational brackets. A capability +built for one is almost always shaped for the other at zero marginal cost to the +producer — true commensalism, and where the flow is folded back into Telperion, +mutualism. + +## Precedents (already fired) + +- **RH → BG:** `IntervalBracketEmitter` (`SqrtBracketCertificate`) regenerated the + BG `e2_two_rhoB` `√2` crux, KERNEL-gated (PR #146). +- **RH → BG:** `IdentityEmitter` (kind=`equation`) discharges BG **RUNG-2** + (`stardom_rung2_family.py`); 972/972 cells validate offline. +- **BG → RH/Telperion:** the StarDom `DirectPolyaEmitter` family + the dual-engine + faithfulness discipline (`target` vs `independent_target`) and the `special=` + first-class-emitter hook are BG-derived shapes now in the shared emitter set. + +## The obligation, concretely + +1. When a proof introduces a recurring hand-written pattern (an identity family, a + positivity/PSD certificate, a bracket, a valuation fact, a monotone/telescope + bound), check whether the sister effort has an obligation of the same *shape* + (see the RH-emitter → BG-obligation map kept alongside the BG proof: + `experiments/graph_hunter/laplacian_ratio/RH_EMITTER_TO_BG_OBLIGATION_MAP.md`). +2. If so, promote the pattern to a first-class emitter kind (or reuse an existing + one) and wire the sister obligation as an `InequalityFamily`. +3. Certify offline (exact arithmetic, no local Lean build), emit frozen Lean, and + let the CI kernel gate confirm. Never hand-edit emitted Lean; fix the family + and regenerate. The proposer is untrusted; the kernel is the only trust. + +## Enforcement + +The manual discipline above is the floor. The proposed **skill-extraction +monitor** (a scheduled proposer agent that scans new proof commits across both +repos for shapes not yet covered by an existing emitter and drafts candidate +families into a quarantine dir for CI confirmation) is the mechanization of this +standing order — see `EMITTER_ROADMAP` / the monitor design when built. diff --git a/telperion/docs/MONITOR_RUN_20260831.md b/telperion/docs/MONITOR_RUN_20260831.md new file mode 100644 index 00000000..9799a699 --- /dev/null +++ b/telperion/docs/MONITOR_RUN_20260831.md @@ -0,0 +1,46 @@ +# Skill-extraction monitor — first run on live 48h corpus (2026-08-31) + +`shape_scout.py` run over 358 Lean files / 18,040 theorems from the current +BG + RH + P-vs-NP work (`telperion/examples/*`, `proof/formalization/R3Cert`, +`rh_lean`). This validates the monitor against work that was NOT hand-mapped. + +## Buckets + +| bucket | count | meaning | +|---|---|---| +| COVERED (emitter-generated) | 13,796 | already automated (frozen telperion output) | +| CANDIDATE (hand-written, emitter-shaped) | 2,881 | proposal queue | +| TRIVIAL (all-numeric) | 282 | norm_num/decide, filtered | +| STRUCTURAL (no emitter) | 1,081 | needs human Lean | + +## What it got right (unsupervised) + +- **Auto-recovered the known RH→BG channels** — with no hand-mapping: + - `valuation` → `BGGateStrictness:deficit_v23_k{1,2,3}` (the 23-adic divisibility + facts) → `emit_padic`. + - `bracket` → `BGRhoBSqrt:bg_rhob_e2_sqrt2_tight`, `SqrtBracket:sqrt_{two,three,ten}` + (the √2 crux, first RH→BG spill) → `emit_bracket`. +- **Firewalled the tree→hub research core** — all 50 `R47R7*` obligations + (`Aobj_child_replace_le`, `strDefect_*`, `DeepPerm` decode) bucketed STRUCTURAL, + no false "I can emit this." Matches the handoff: two genuine research obligations, + everything structural around them proven. + +## New lead surfaced (+ classifier fix) + +- **P-vs-NP joins the shared engine.** `Hsq.lean:hsq_of_subsetForm` — + `∀ s, s.totalDegree ≤ d → 0 ≤ pe nq (s²)` — is a **pseudo-expectation + sum-of-squares** obligation (the SoS-3XOR / P-vs-NP lane). It is SOS-shaped, i.e. + the **same box-positivity/SOS engine** BG's `bg_bulk_discharge` and RH's zero-free + region use. The monitor initially mis-labeled it `interlacing`; `classify()` now + routes `0 ≤ pe(… ^ 2)` to `sos_psd` → `SOSEmitter`. +- Consequence: the shared-engine reassessment now spans **three programs** — + RH (zero-free `(1+x)^n` Handelman), BG (bulk-discharge `φ_v ≤ F*`), and P-vs-NP + (SoS pseudo-expectation `0 ≤ pe(s²)`) — all box-positivity / SOS. The 23-adic tie + remains BG-internal (BG↔Φ¹¹); the engine is the three-way meeting point. + +## Honest scope + +CANDIDATE ≠ closed. The 2,881 candidates are shape-matched, not certified; the value +gate is the offline certify round-trip (`--certify`) then the CI kernel. The +STRUCTURAL core (tree→hub, the tight-τ discharge rule) is the real open research and +no emitter reaches it. `conjecture1_proved = False`. diff --git a/telperion/docs/SKILL_EXTRACTION_MONITOR.md b/telperion/docs/SKILL_EXTRACTION_MONITOR.md new file mode 100644 index 00000000..2b9bde82 --- /dev/null +++ b/telperion/docs/SKILL_EXTRACTION_MONITOR.md @@ -0,0 +1,99 @@ +# Skill-extraction monitor — design + evidence-first findings + +Mechanizes the [cross-pollination standing order](CROSS_POLLINATION_STANDING_ORDER.md): +continuously watch BG + RH proof work, surface shapes an existing (or new) Telperion +emitter could discharge, and feed a proposal queue for offline certification + CI +kernel confirmation. + +## Architecture (proposer, not mechanical daemon) + +The judgment step — "is this recurring hand-written pattern a generalizable shape?" +— is LLM-shaped, and the trust boundary is binding. So the monitor is a **scheduled +proposer agent** wrapping a deterministic **extraction+dedup core**: + +``` + new proof commit (BG or RH repo) + │ (git post-commit trigger, or low-freq schedule) + ▼ + [1] shape_scout.py ← deterministic core (this dir, stdlib-only) + │ extract theorem goals · classify into emitter SHAPE · + │ dedup vs emitter-GENERATED files (telperion provenance header) + ▼ + CANDIDATE queue (hand-written, emitter-shaped, non-trivial) + │ + [2] agent triage ← LLM: cluster candidates into a would-be FAMILY; + │ pick/propose an emitter kind; draft an InequalityFamily + ▼ + [3] offline certify ← REAL dedup: does the emitter actually REPRODUCE the goal? + │ (exact Fraction/sympy; no Lean build) emitter-shaped + │ ≠ emitter-reproducible — this step is the true filter. + ▼ + telperion/candidates/ ← QUARANTINE (untrusted). Never auto-registered. + │ + [4] CI kernel gate ← rh-compiles / lean-verify-*: the ONLY trusted step. + ▼ + human promotes to the shared emitter set +``` + +The proposer stays strictly untrusted: it drafts candidate families into a +quarantine dir, never hand-writes emitted Lean, never registers a trusted emitter. +The kernel is the sole arbiter. + +## The core: `tools/shape_scout.py` + +Stdlib-only. Walks Lean roots, extracts each theorem's goal (depth-0 bracket scan +for the goal-opening `:` … `:=`), strips Lean comments first (so `theorem` inside a +docstring is never mistaken for a declaration), classifies the goal into a shape, +and buckets: + +- **COVERED** — in an emitter-generated file (telperion provenance header). Done. +- **CANDIDATE** — hand-written, emitter-shaped, non-trivial. The proposal queue. +- **TRIVIAL** — all-numeric constant fact (norm_num/decide), no big integer. Filtered. +- **STRUCTURAL** — not inequality/identity-shaped (encoder, def-bridge, ∀-over- + inductive). No emitter reaches it — the `hConfine` bucket. + +Shape → emitter map covers: `identity`→IdentityEmitter, `polya_ineq`→DirectPolya/ +bilinear, `sos_psd`→SOS/WorstCorner, `bracket`→IntervalBracket, `valuation`→padic, +`trig_nonneg`, `interlacing`, `unimodal`, `witness`, `monotone`. + +## Measured evidence (2026-08-30, first run) + +Run against RH (`rh_lean/RH`, 25 files) and BG (`laplacian_ratio/formalization`, +240 files) corpora. + +| corpus | scanned | covered | candidate | trivial | structural | +|---|---|---|---|---|---| +| RH | 116 | 22 | **54** | 30 | 10 | +| BG | 7137 | 1944 | **3777** | 371 | 1045 | + +Genuine cross-pollination gold surfaced in the RH corpus (the BG modules riding in +the RH gate): `deficit_v23_k*` (valuation → emit_padic), `tie_collective_balance` +(identity → IdentityEmitter), `log_*_enclosure` / `bg_omega_enclosure` (bracket → +IntervalBracket), `hankel_jensen_xi_n0_H*` (PSD). + +### False-positive classes (measured, and status) + +1. **Prose/extraction noise** — `theorem`/`lemma` inside docstrings (BG's `Lean` + artifact). Was ~23% of BG raw candidates. **FIXED** by `_strip_comments` + (BG theorem count 7167→7137; noise class eliminated). +2. **All-numeric triviality** — rational-constant comparisons closable by + `norm_num`. Was ~77% of RH raw candidates. **FIXED** by `is_trivial` (keeps + large-integer valuation/identity facts, which emit_padic/IdentityEmitter handle + better than raw norm_num). +3. **Definitional recursion equations** over inductive types (`rho0_node`, + `realize_node` with `Branch.node`) misclassified as rational identities. + **RESIDUAL** — next filter; cleanly detectable by constructor-presence + (RHS/LHS mentions a data constructor ⇒ definitional `rfl`/`simp`, not an emitter + target). + +## Gating decision (before wiring the schedule) + +1. Add the constructor/definitional filter (FP class 3). +2. Wire step [3] — the offline certify round-trip — as the true dedup. "Emitter- + shaped" (structural) ≠ "emitter-reproducible" (certified). Only a candidate an + emitter actually reproduces offline enters quarantine. +3. Trigger on new proof commits, not every session (cache-window economics); the + monitor writes only to `candidates/`, never to proof branches (parallel-session + collision safety). + +The deterministic core is viable today; the schedule is a thin wrapper once 1–3 land. diff --git a/telperion/docs/probes/sos_pe_probe.py b/telperion/docs/probes/sos_pe_probe.py new file mode 100644 index 00000000..d715365c --- /dev/null +++ b/telperion/docs/probes/sos_pe_probe.py @@ -0,0 +1,94 @@ +"""Probe: the P-vs-NP SoS pseudo-expectation obligation `0 <= pe(s^2)` certifies via +the SAME exact-rational PSD/SOS engine RH's Weil/Jensen minors and BG's SOS base use. + +Validates the monitor's shape-match (Hsq.lean:hsq_of_subsetForm) with a concrete +instance, parallel to the BG Handelman probe. `0 <= pe(s^2)` for all degree-<=d s +<=> the degree-2d moment matrix M[u,v] = pe(x_u x_v) is PSD. We build M for a small +satisfiable 3-XOR pseudo-expectation and certify PSD by an EXACT rational LDL^T (all +pivots >= 0) -- an SOS/PSD Gram certificate, the emit_sos / WorstCorner shape. +Offline, exact rationals. +""" +import itertools +from fractions import Fraction as F +import sympy as sp + +# ---- a small satisfiable 3-XOR: x1 x2 x3 = 1, xi in {+-1}. A 2-point mixture of +# solutions (not the fully-symmetric measure, which collapses to the identity) gives a +# STRUCTURED rank-deficient PSD moment matrix -- a genuine SoS-boundary object. ---- +sols = [(1, 1, 1), (1, -1, -1)] # both satisfy x1 x2 x3 = 1 +w = [F(1, 2), F(1, 2)] # mixture weights (pe = sum_k w_k eval_{sols[k]}) +def pe(monomial_idx): + """pseudo-expectation of prod_{i in idx} x_i under the mixture measure (exact).""" + tot = F(0) + for wk, s in zip(w, sols): + p = 1 + for i in monomial_idx: + p *= s[i] + tot += wk * p + return tot + +# degree-1 monomial basis: 1, x1, x2, x3 (indices: () , (0,), (1,), (2,)) +basis = [(), (0,), (1,), (2,)] +def mono_mul(a, b): + # x_i^2 = 1 (spins): symmetric difference of index multisets + from collections import Counter + c = Counter(a) + Counter(b) + return tuple(sorted(i for i, k in c.items() if k % 2)) + +# moment matrix M[u,v] = pe(basis_u * basis_v), exact rational +n = len(basis) +M = [[pe(mono_mul(basis[i], basis[j])) for j in range(n)] for i in range(n)] +print("moment matrix M (pe(x_u x_v), exact):") +for row in M: + print(" ", [str(x) for x in row]) + +# ---- EXACT rational LDL^T: PSD iff all pivots >= 0 (the PSD/SOS certificate) ---- +import copy +A = copy.deepcopy(M) +L = [[F(0)]*n for _ in range(n)] +D = [F(0)]*n +psd = True +for j in range(n): + d = A[j][j] - sum(L[j][k]**2 * D[k] for k in range(j)) + D[j] = d + L[j][j] = F(1) + if d < 0: + psd = False + for i in range(j+1, n): + if d == 0: + L[i][j] = F(0) + else: + L[i][j] = (A[i][j] - sum(L[i][k]*L[j][k]*D[k] for k in range(j))) / d +print(f"\nexact LDL^T pivots D = {[str(x) for x in D]}") +print(f"all pivots >= 0 -> moment matrix PSD: {psd and all(x >= 0 for x in D)}") + +# ---- 0 <= pe(s^2) for a sample s = x1 - x2 (=> c^T M c with c over basis) ---- +c = {(0,): F(1), (1,): F(-1)} +# pe((x1 - x2)^2) = pe(x1^2) - 2 pe(x1 x2) + pe(x2^2) +val = pe((0,0)) - 2*pe((0,1)) + pe((1,1)) +cvec = [c.get(b, F(0)) for b in basis] +quad = sum(cvec[i]*cvec[j]*M[i][j] for i in range(n) for j in range(n)) +print(f"\npe((x1 - x2)^2) = {val} (direct) == c^T M c = {quad} (moment form): {val == quad}") +print(f"0 <= pe((x1 - x2)^2): {val >= 0}") + +# ---- SOS reading: M = sum_k D_k (L col_k)(L col_k)^T is an SOS/PSD Gram (emit_sos shape) ---- +sy = sp.symbols("one x1 x2 x3") +vec = sp.Matrix([1, sy[1], sy[2], sy[3]]) +Msym = sp.Matrix([[sp.Rational(M[i][j].numerator, M[i][j].denominator) for j in range(n)] for i in range(n)]) +quad_poly = sp.expand((vec.T * Msym * vec)[0]) +sos = sum(sp.Rational(D[k].numerator, D[k].denominator) * + (sum(sp.Rational(L[i][k].numerator, L[i][k].denominator)*vec[i] for i in range(n)))**2 + for k in range(n)) +print(f"\nSOS/PSD Gram certificate (M = sum_k D_k v_k v_k^T) reconstructs the moment form exactly: " + f"{sp.expand(quad_poly - sos) == 0}") +print("\n=== VERDICT: the SoS pseudo-expectation `0 <= pe(s^2)` IS the exact-rational PSD/SOS") +print("engine (LDL^T pivots >= 0 = SOS Gram) -- same shape as RH Weil/Jensen minors + BG SOS base.") +print("Three programs (RH zero-free, BG bulk-discharge, P-vs-NP SoS), one box-positivity/SOS engine.") +print(""" +HONEST SCOPE (cf. the BG owner's caveat 1): this instance is EASY -- a satisfiable +3-XOR whose pe is a real measure, so PSD is automatic. It demonstrates the ENGINE +(the shape reduces to exact PSD/SOS), not a hard result. The hard P-vs-NP content is +the SoS degree LOWER BOUND: constructing a pe for an UNSAT expanding instance that +keeps the moment matrix PSD through degree d (the tight moment-SDP feasibility) -- +exactly analogous to BG's open tight field-tau. The engine certifies the atoms; the +hard construction is the open research. conjecture1_proved = False.""") diff --git a/telperion/tools/shape_scout.py b/telperion/tools/shape_scout.py new file mode 100644 index 00000000..b7334112 --- /dev/null +++ b/telperion/tools/shape_scout.py @@ -0,0 +1,477 @@ +#!/usr/bin/env python3 +"""shape_scout: the extraction+dedup core of the Telperion skill-extraction monitor. + +Scans Lean proof corpora (BG and RH), extracts each theorem's GOAL, classifies it +into a Telperion emitter SHAPE, and separates: + + COVERED theorem lives in an emitter-GENERATED file (telperion provenance + header) -> already automated, nothing to do. + CANDIDATE hand-written theorem whose goal IS emitter-shaped -> a cross- + pollination proposal: an existing emitter kind could (re)generate it. + STRUCTURAL hand-written theorem that is NOT inequality/identity-shaped (encoder, + def-bridge, forall-over-inductive, iff of structures) -> no emitter + reaches it; needs human Lean. (The `hConfine` bucket.) + +This is the UNTRUSTED proposer only. It never emits trusted Lean; it produces a +proposal queue for offline certification + CI-kernel confirmation. + +Usage: + python3 shape_scout.py [ ...] [--json out.json] + +Stdlib only. Classification is structural/textual (no sympy, no Lean build). +""" +from __future__ import annotations + +import argparse +import json +import re +import sys +from dataclasses import dataclass, field +from pathlib import Path + +# --- Telperion emitter-kind vocabulary (the shapes we can already discharge) ---- +# Maps a shape label -> the emitter module/kind that handles it. Anything not +# here is STRUCTURAL (not emitter-shaped). +EMITTER_FOR = { + "identity": "emit_facts.IdentityEmitter (kind=equation)", + "polya_ineq": "emit.DirectPolyaEmitter (kind=direct) / bilinear box", + "sos_psd": "emit_sos.SOSEmitter / psd_form / WorstCorner", + "bracket": "emit_bracket.IntervalBracketEmitter (kind=bracket)", + "valuation": "emit_padic (kind=valuation)", + "trig_nonneg": "emit_sos_refutation / trig_nonneg (Markov-Lukacs)", + "interlacing": "emit_interlacing (real-rootedness)", + "unimodal": "emit_unimodal (special=unimodal)", + "witness": "witness kind (existential comparator)", + "monotone": "emit_monotone_tail", +} + +PROVENANCE = re.compile(r"/-\s*telperion", re.I) + +# A Lean theorem/lemma header up to the goal-opening `:`. We then bracket-scan. +THM = re.compile(r"\b(?:theorem|lemma)\s+([A-Za-z0-9_'.]+)", re.M) + +OPEN, CLOSE = "([{⟨", ")]}⟩" + + +def _strip_comments(src: str) -> str: + """Remove Lean block (/- ... -/, nested) and line (-- ...) comments so that the + word 'theorem' inside a docstring is never mistaken for a real declaration. + Run AFTER provenance detection (which reads the raw header).""" + out = [] + i, n, depth = 0, len(src), 0 + while i < n: + two = src[i:i + 2] + if depth == 0 and two == "--": + j = src.find("\n", i) + i = n if j < 0 else j + continue + if two == "/-": + depth += 1 + i += 2 + continue + if two == "-/" and depth > 0: + depth -= 1 + i += 2 + continue + if depth == 0: + out.append(src[i]) + i += 1 + return "".join(out) + + +_INT = re.compile(r"\d+") +_FREEVAR = re.compile(r"\(\s*[a-zA-Z]\w*\s*[:)]|\b[a-z]\w*\s+[a-z]\w*\b") + +# Data-constructor token: `Type.ctor` (Branch.node, RTree.node, Equiv.swap) or a +# capitalized collection/constructor identifier used in constructor position +# (Multiset, `List.`). Used to keep DEFINITIONAL recursion equations over +# inductive types (rfl/simp lemmas, NOT rational-function identities an emitter +# can reproduce) out of the `identity` CANDIDATE queue -- they are STRUCTURAL. +# Conservative: `Type.ctor` requires an UPPER-case type head so ordinary +# lower-case function application (`rRoot a i cs`, `Real.log`) is not caught. +_CONSTRUCTOR = re.compile(r"\b[A-Z][A-Za-z0-9_]*\.[a-z]|\bMultiset\b|\bList\.") + + +def is_trivial(goal: str, shape: str) -> bool: + """All-numeric constant fact closable by norm_num/decide -> NOT an emitter gap. + Large-integer valuation/identity facts are kept genuine (emit_padic / IdentityEmitter + handle them better than raw norm_num, and they are the real BG tie signal).""" + if shape in ("valuation",): + return False + if _FREEVAR.search(goal): + return False + ints = [int(m.group()) for m in _INT.finditer(goal)] + big = any(v > 10_000 for v in ints) + return not big # all-numeric AND no big integer -> trivial norm_num fact + + +def _extract_goal(src: str, start: int) -> tuple[str, str] | None: + """From the char index just after a theorem NAME, return (name-less) GOAL text + and the tactic head, by depth-0 scanning for the goal-opening ':' then ':='.""" + depth = 0 + i = start + goal_start = None + n = len(src) + while i < n: + c = src[i] + if c in OPEN: + depth += 1 + elif c in CLOSE: + depth -= 1 + elif depth == 0 and c == ":" and src[i:i + 2] != ":=": + goal_start = i + 1 + break + i += 1 + if goal_start is None: + return None + # find depth-0 ':=' ending the goal + depth = 0 + j = goal_start + while j < n: + c = src[j] + if c in OPEN: + depth += 1 + elif c in CLOSE: + depth -= 1 + elif depth == 0 and src[j:j + 2] == ":=": + goal = src[goal_start:j] + tac = src[j + 2:j + 60].strip().split("\n")[0] + return goal.strip(), tac + j += 1 + return None + + +def classify(goal: str) -> str: + """Structural heuristics -> shape label. Order matters (most specific first).""" + g = goal + # p-adic / divisibility + if re.search(r"∣|padicVal|factorization|Nat\.gcd|Coprime", g): + return "valuation" + # PSD / matrices / minors + if re.search(r"PosSemidef|Matrix|\bdet\b|Gram|minor|IsHermitian", g): + return "sos_psd" + # SOS / pseudo-expectation nonnegativity-on-squares: `0 ≤ pe(.. ^ 2)` (SoS-3XOR + # / P-vs-NP lane) is an SOS certificate shape, NOT interlacing -- route to the + # same SOS engine BG's bulk-discharge and RH's zero-free region use. + if re.search(r"0\s*≤", g) and re.search(r"\bpe\b|pseudo|Expect", g) and "^ 2" in g: + return "sos_psd" + # bracket: two-sided enclosure of a transcendental + if re.search(r"sqrt|Real\.exp|Real\.log|π|Real\.pi|Gamma|zeta|ζ", g) and ( + g.count("≤") + g.count("<") >= 2 or "∧" in g + ): + return "bracket" + # nonneg trig + if re.search(r"cos|sin", g) and re.search(r"0\s*≤|≥\s*0", g): + return "trig_nonneg" + # real-rootedness / interlacing + if re.search(r"roots|Polynomial|interlac|hyperbolic|separ", g, re.I): + return "interlacing" + # unimodal / single-crossing + if re.search(r"unimodal|StrictMono.*StrictAnti|crosses", g, re.I): + return "unimodal" + # existential witness + if re.search(r"^\s*∃|\b∃", g): + return "witness" + # identity: a top-level '=' that is not ≤/≥/≠/≈ and not an iff + eqs = re.findall(r"(?:=])=(?![=])", g) + if eqs and "↔" not in g and not re.search(r"≤|<|≥|>", g): + # DEFINITIONAL recursion equation over an inductive type (either side + # mentions a data constructor, e.g. `rho0 (Branch.node c ch) = ...`)? + # That is a rfl/simp lemma, not a rational-function identity the + # IdentityEmitter can reproduce -> STRUCTURAL, not a CANDIDATE. + # Pure arithmetic identities over ℚ/ℝ (no constructor token) stay `identity`. + if _CONSTRUCTOR.search(g): + return "structural" + return "identity" + # monotone tail + if re.search(r"Monotone|Antitone|Tendsto|tail", g): + return "monotone" + # generic polynomial/rational inequality over reals + if re.search(r"≤|<|≥|>", g) and re.search(r"ℝ|ℚ|\(\s*x|\by\b", g): + return "polya_ineq" + # structural: iff of props, forall over inductive, function/encoder, set eq + return "structural" + + +@dataclass +class ThmRec: + name: str + file: str + shape: str + emitted: bool + goal_excerpt: str + goal_full: str = "" # untruncated goal (one-line normalized) for --certify + + +@dataclass +class Report: + thms: list[ThmRec] = field(default_factory=list) + + def scan_file(self, path: Path): + raw = path.read_text(errors="replace") + emitted = bool(PROVENANCE.search(raw[:400])) + src = _strip_comments(raw) + for m in THM.finditer(src): + name = m.group(1) + res = _extract_goal(src, m.end()) + if not res: + continue + goal, _tac = res + shape = classify(goal) + flat = re.sub(r"\s+", " ", goal).strip() + self.thms.append(ThmRec( + name=name, file=path.name, shape=shape, emitted=emitted, + goal_excerpt=flat[:110], goal_full=flat, + )) + + def buckets(self): + covered, candidate, structural, trivial = [], [], [], [] + for t in self.thms: + if t.emitted: + covered.append(t) + elif t.shape == "structural": + structural.append(t) + elif is_trivial(t.goal_excerpt, t.shape): + trivial.append(t) + else: + candidate.append(t) + return covered, candidate, structural, trivial + + +# =========================================================================== +# --certify : offline round-trip. "emitter-SHAPED" != "emitter-REPRODUCIBLE". +# For CANDIDATE goals in a tractable arithmetic fragment, translate the Lean +# goal text into a sympy expression and actually run the check an emitter would +# rely on: +# * identity goal `LHS = RHS` -> sympy.simplify(LHS - RHS) == 0 (this is +# exactly what Telperion's `equation`-kind certify validates). +# * inequality `0 <= E` / `A <= B` / `A < B` -> Telperion's real Polya +# positivity certify (`telperion.certify.polya_certify`) over the nonneg +# orthant in x, y; if that refuses, a HEURISTIC numeric sampling fallback. +# Everything with function symbols / transcendentals / constructors / unknown +# identifiers is OUT-OF-FRAGMENT (not attempted, NOT a failure). +# =========================================================================== + +# Free symbols the fragment admits (declared nonnegative for Polya). Any OTHER +# alphabetic identifier => out-of-fragment (it is a function symbol or unknown). +_ALLOWED_SYMS = ("x", "y") + +# Tokens that immediately disqualify a goal from the arithmetic fragment. +_OUT_OF_FRAGMENT = re.compile( + r"∑|∏|∫|√|Real\.|Complex\.|riemannZeta|Gamma|Nat\.|Int\.|Finset|Multiset|" + r"List\.|Matrix|max\b|min\b|∣|∀|∃|↔|→|if\b|then\b|fun\b|λ|‖|⌊|⌈|" + r"[A-Z][A-Za-z0-9_]*\.[a-z]|::" +) + + +def _lean_to_sympy_str(side: str) -> str: + """Turn one Lean arithmetic side into a python/sympy-eval string, or raise + ValueError if it leaves the fragment. Handles: `(a : ℚ)/b`, `(a:ℝ)`, + bare ints, + - * / ^ (=> **), parentheses, and free symbols x, y. + + The result is eval'd in a namespace containing ONLY sympy Rational + the two + symbols, so a stray identifier raises NameError even if it slips past here. + """ + s = side.strip() + # strip type ascriptions: (E : ℚ) -> (E) ; bare `: ℝ` / `: ℚ` -> '' + s = re.sub(r":\s*[ℚℝℤℕ]", "", s) + s = s.replace("ℚ", "").replace("ℝ", "").replace("ℤ", "").replace("ℕ", "") + # power operator + s = s.replace("^", "**") + # reject anything outside the arithmetic grammar (after ascription strip): + # digits, the two allowed symbols, operators, parens, whitespace, dot(float) + leftover = re.sub(r"[0-9xy\s()+\-*/.]", "", s) + if leftover: + raise ValueError(f"non-arithmetic token(s): {sorted(set(leftover))!r}") + # bare-integer literals as sympy Rationals so `64/621` is exact, not float + s = re.sub(r"(?≥≠:" or goal[idx + 1:idx + 2] == "="): + continue + return goal[:idx].strip(), rel, goal[idx + 1:].strip() + return None + + +def certify_candidate(goal: str): + """Attempt an offline round-trip of one CANDIDATE goal. + + Returns a dict {status, check, detail} where status is one of: + reproduced -- identity simplifies to 0, or inequality carries a Polya + certificate (or heuristic sampling found no violation). + contradicted -- identity does NOT simplify to 0, or sampling found a + negative point => RED FLAG (misclassification or a + genuinely non-reproducible goal). + out_of_fragment -- has function symbols/transcendentals/etc; not attempted. + """ + if _OUT_OF_FRAGMENT.search(goal): + return {"status": "out_of_fragment", "check": "-", "detail": "non-arithmetic token"} + rel = _split_relation(goal) + if rel is None: + return {"status": "out_of_fragment", "check": "-", "detail": "no single relation / bracket"} + lhs, op, rhs = rel + try: + import sympy as sp + except ImportError: + return {"status": "out_of_fragment", "check": "-", "detail": "sympy unavailable"} + syms = {"x": sp.Symbol("x", nonnegative=True), "y": sp.Symbol("y", nonnegative=True)} + try: + L = _eval_side(lhs, sp, syms) + R = _eval_side(rhs, sp, syms) + except (ValueError, NameError, SyntaxError, TypeError, ZeroDivisionError) as e: + return {"status": "out_of_fragment", "check": "-", "detail": f"translate: {e}"} + + if op == "=": + try: + zero = sp.simplify(L - R) == 0 + except Exception as e: # noqa: BLE001 + return {"status": "out_of_fragment", "check": "sympy.simplify", "detail": str(e)} + if zero: + return {"status": "reproduced", "check": "sympy.simplify(LHS-RHS)==0", + "detail": "identity"} + return {"status": "contradicted", "check": "sympy.simplify(LHS-RHS)==0", + "detail": f"LHS-RHS = {sp.nsimplify(sp.simplify(L - R))}"} + + # inequality op in {<=, <}: normalize to 0 <= E (E = R - L) + E = sp.expand(R - L) + used_syms = [s for s in (syms["x"], syms["y"]) if s in E.free_symbols] + # (1) real Telperion Polya positivity certify + try: + sys.path.insert(0, __import__("os").path.expanduser("~/repos/Arda/telperion/src")) + from telperion.certify import polya_certify + polya_certify(E, used_syms, lift_max=2) + return {"status": "reproduced", "check": "telperion.polya_certify", + "detail": f"0 <= {E} (Polya certificate)"} + except ValueError as e: + polya_detail = f"polya refused: {e}" + except Exception as e: # noqa: BLE001 (import/other) -> fall through to heuristic + polya_detail = f"polya n/a: {e}" + # (2) HEURISTIC numeric sampling fallback over the nonneg orthant. + try: + import random + f = sp.lambdify(used_syms, E, "math") if used_syms else None + worst = None + pts = 400 if used_syms else 1 + for _ in range(pts): + vals = [random.uniform(0, 12) for _ in used_syms] + v = float(f(*vals)) if f else float(E) + if worst is None or v < worst[0]: + worst = (v, vals) + if worst is not None and worst[0] < -1e-9: + return {"status": "contradicted", "check": "numeric-sampling(HEURISTIC)", + "detail": f"negative at {dict(zip([str(s) for s in used_syms], worst[1]))}: {worst[0]:.4g}; {polya_detail}"} + return {"status": "reproduced", "check": "numeric-sampling(HEURISTIC)", + "detail": f"no violation in 400 nonneg samples (min {worst[0]:.4g}); {polya_detail}"} + except Exception as e: # noqa: BLE001 + return {"status": "out_of_fragment", "check": "-", "detail": f"sampling failed: {e}; {polya_detail}"} + + +def run_certify(candidate, show: int) -> None: + from collections import Counter + results = [] + for t in candidate: + r = certify_candidate(t.goal_full or t.goal_excerpt) + results.append((t, r)) + n = len(results) + status = Counter(r["status"] for _, r in results) + in_frag = status["reproduced"] + status["contradicted"] + print("\n=== --certify : offline round-trip ('shaped' -> 'reproducible') ===") + print(f" candidates {n:4d}") + print(f" in-fragment (attempted) {in_frag:4d}") + print(f" reproduced (round-trip) {status['reproduced']:4d}") + print(f" CONTRADICTED (RED FLAG) {status['contradicted']:4d}") + print(f" out-of-fragment (skipped) {status['out_of_fragment']:4d}") + frac = (status["reproduced"] / in_frag) if in_frag else 0.0 + print(f" reproducible fraction (of in-fragment): {frac:.1%}") + + checks = Counter(r["check"] for _, r in results if r["status"] in ("reproduced", "contradicted")) + if checks: + print(" checks used:") + for c, k in checks.most_common(): + print(f" {k:4d} {c}") + + contra = [(t, r) for t, r in results if r["status"] == "contradicted"] + if contra: + print(f"\n RED FLAGS -- CONTRADICTED candidates ({len(contra)}):") + for t, r in contra: + print(f" [{r['check']}] {t.file}:{t.name}") + print(f" goal: {t.goal_full[:120]}") + print(f" why : {r['detail']}") + else: + print("\n RED FLAGS: none (no in-fragment candidate contradicted).") + + repro = [(t, r) for t, r in results if r["status"] == "reproduced"] + if show and repro: + print(f"\n sample REPRODUCED (first {show}):") + for t, r in repro[:show]: + print(f" [{r['check']}] {t.file}:{t.name}") + print(f" {t.goal_full[:110]}") + + +def main(argv=None) -> int: + ap = argparse.ArgumentParser() + ap.add_argument("roots", nargs="+") + ap.add_argument("--json") + ap.add_argument("--show", type=int, default=12, help="candidate examples to print") + ap.add_argument("--certify", action="store_true", + help="offline round-trip: sympy/Polya-certify in-fragment candidates") + args = ap.parse_args(argv) + + rep = Report() + for root in args.roots: + for p in sorted(Path(root).rglob("*.lean")): + rep.scan_file(p) + + covered, candidate, structural, trivial = rep.buckets() + total = len(rep.thms) + print(f"scanned {total} theorems across {len(args.roots)} root(s)") + print(f" COVERED (emitter-generated) {len(covered):4d}") + print(f" CANDIDATE (hand-written, emitter-shaped) {len(candidate):4d} <- proposal queue") + print(f" TRIVIAL (all-numeric, norm_num/decide) {len(trivial):4d} (filtered out)") + print(f" STRUCTURAL(hand-written, no emitter) {len(structural):4d}") + + from collections import Counter + print("\ncandidate shapes (what an existing emitter could regenerate):") + for shape, n in Counter(t.shape for t in candidate).most_common(): + print(f" {n:4d} {shape:12s} -> {EMITTER_FOR.get(shape, '?')}") + + print(f"\nsample candidates (first {args.show}):") + for t in candidate[:args.show]: + print(f" [{t.shape:11s}] {t.file}:{t.name}") + print(f" {t.goal_excerpt}") + + if args.certify: + run_certify(candidate, args.show) + + if args.json: + Path(args.json).write_text(json.dumps({ + "totals": {"covered": len(covered), "candidate": len(candidate), + "structural": len(structural)}, + "candidates": [t.__dict__ for t in candidate], + "structural": [t.__dict__ for t in structural], + }, indent=2)) + print(f"\nwrote {args.json}") + return 0 + + +if __name__ == "__main__": + sys.exit(main())