Auditable proof structure · local prototypes

Proof Graph Laboratory / Mathematical Motifs

Treat the verified library as an instrument for asking whether a target-faithful proof is a coverage extension, a library consolidation, or evidence of irreducible reusable proof structure.

Evidence boundary. The graph is environment-extracted from compiled declaration types and values; it is not a kernel trace or an elaborator trace. Proof-cost, ZDD, hypergraph/MIP, and novelty operations are prototypes, not Lean theorems or validated scientific scores.

Frozen exact-dependency observation

The baseline is cb5d50be148c691cc595ed9fd2f535c42506fada; the deterministic graph artifact has SHA-256 177233bc84b7f18928f66b1bf95545095d7dd1373f32d7dd2ed286c46bc520c9. Project ownership comes from the loaded Lean environment, with signature/type and value/proof dependencies kept separate.

13,512project-owned declarations

4,309direct external boundary declarations

664,837direct type/value edges

2,237module import records

Fixed compiled benchmark

These terminals are unchanged observations, not claims that each complete algorithm family is formalized. The union charges each compiled declaration once: 1,238 standalone support memberships compress to 1,046 union declarations, with 175 declarations shared by at least two routes.

EXP3 · compiled root

exp3_realized_all_time

Existing all-time realized-regret failure-set bound; benchmark only, theorem unchanged.

Project support: 421 declarations
Shared support: 170 (40.4%)
Semantic DAG: 421 components · depth 23
Proof-term proxy: 238,985 shared objects
Local Lean check: 24.769332 seconds · one warm-dependency run

half-Tsallis · compiled root

half_tsallis_iid_log

Existing finite-arm IID half-Tsallis logarithmic expected-regret declaration; benchmark only, theorem unchanged.

Project support: 505 declarations
Shared support: 134 (26.5%)
Semantic DAG: 505 components · depth 30
Proof-term proxy: 341,127 shared objects
Local Lean check: 22.424018 seconds · one warm-dependency run

OFUL · compiled root

oful_all_time_confidence

Existing canonical-history all-time confidence failure-set declaration; benchmark only, theorem unchanged.

Project support: 312 declarations
Shared support: 63 (20.2%)
Semantic DAG: 312 components · depth 26
Proof-term proxy: 188,840 shared objects
Local Lean check: 22.872432 seconds · one warm-dependency run

ZDD support families and hypergraph lower bounds

The ZDD contains only minimal support sets over a fixed declaration universe. Metavariables, tactics, unification constraints, and other dependent proof state remain outside. Local time and tracemalloc values are implementation observations, not universal complexity claims.

Variable order	ZDD nodes	Serialized proxy bytes	Local peak bytes
lexical	1,238	55,872	837,910
frequency_desc	1,163	52,367	773,180
frequency_asc	1,173	52,881	736,544
first_seen	1,238	55,882	739,004

The unit-charge hypergraph exact optimum is 1,046; both reported admissible lower bounds are 505 on this benchmark. Every concrete completion is tested to map to the relaxation. Pruning is called safe only under the explicit contract LB(s) <= OPT_remaining(s). The MIP is a library planner/scheduler, not a Lean elaborator.

Non-scalar proof-structural novelty audit

Raw new-node count is excluded: helper names and proof splitting can manipulate it. The fixed vector keeps five questions separate: conditional residual signatures with separately audited irreducibility; backward compression; proof-cost Pareto-frontier shift; held-out transfer; and target novelty versus proof novelty.

Freeze the library at t.Freeze statements, assumptions, canonicalization, compression, and benchmark roots before comparison.
Audit residual structure.Compare canonical lemma motifs, support hyperedges, obligation types, and composition constraints—not declaration names.
Test backward compression and Pareto movement.Report every declared cost dimension, including check time and open obligations, without scalarizing reuse into an unbounded reward.
Transfer to held-out theorems.Do not use the held-out family to design the abstraction; disclose failures and unlocked obligations.
Review interpretability.Run ordering/compression ablations and blind human review before assigning a neutral grade.

Neutral audit grades:

coverage extension
library consolidation
new proof route
reusable abstraction
cross-family conceptual compression

Candidate reusable abstraction

Curvature–Noise–Gap finite geometry

Partial

A route-independent finite algebra layer is compiled after the frozen graph. A name-independent two-round structural proxy observes 9 new color signatures and 5 new direct-support signatures, but does not establish semantic irreducibility. All three frozen benchmark structural supports are unchanged, existing-to-CNG dependency edges are zero, and held-out OFUL contains zero CNG declarations; backward compression and transfer are not demonstrated, the full Pareto relation is not assessed, and structural discovery is not established.

Current falsification result. The fixed two-round name-independent proxy finds 9 new neighborhood-color signatures and 5 new direct-support signatures, but explicitly does not establish irreducibility. All frozen benchmark closures are unchanged; there are 0 existing-to-CNG dependency edges and 0 CNG declarations in the held-out OFUL support. Structural discovery remains false.

Falsifiable upgrade rule. CNG becomes structural-discovery evidence only if it replaces multiple audited route-specific subgraphs, improves the declared cost vector with a reported Pareto relation, and helps a theorem family held out from design or unlocks a blocked obligation. Merely restating a Tsallis-INF derivation does not qualify.

Local execution and static Pages boundary

This page renders versioned JSON summaries. Static GitHub Pages does not load a Lean environment, regenerate the graph, execute the ZDD/hypergraph prototype, solve a MIP, or certify novelty. Reproduce those observations locally after the Lean gate:

lake build BanditRLProof
lake env lean --run tools/ProofGraphExport.lean --compact proof-graph.json
python tools/proof_graph_lab.py validate-export --graph proof-graph.json
python tools/proof_graph_lab.py benchmark --graph proof-graph.json --config research-wiki/proof-graph/benchmark_roots.json --measurements research-wiki/proof-graph/benchmark_measurements.json --output benchmark-report.json

The laboratory explicitly excludes Chapters 13–17, finite-arm lower bounds, Bernoulli-KL/change-of-measure/minimax/asymptotic lower-bound declarations, their cards/pages, and the lower-bound task's active frontier.