Telperion skill-extraction monitor + cross-pollination synthesis

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.

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.

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`.

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.