theorem-synthesis

Theorem Synthesis

Promote a new positive statement by proving the missing glue between accepted claims. Keep proof, empirical applicability, and scientific interpretation distinct so each can advance without becoming ceremony for the others. Protect the strongest useful theorem supported by the composition; do not make a proof easier by shrinking the result to a tautology or isolated special value.

Establish the target

Read AGENTS.md, governance/releases/current.yaml, the relevant entries in governance/claims.yaml, and .agents/skills/physics-erdos-loop/SKILL.md. Instantiate memory-templates/theorem-synthesis.md and a synthesis proposal manifest before substantive proof work.

State:

• one exact higher theorem;
• at least two distinct accepted dependency claims;
• the structural gap not closed by any accepted claim;
• assumptions, exclusions, and intended consumers;
• core or interpretive layer, with a named hypothesis for the latter.

Do not re-review accepted dependencies. Audit only that the theorem uses their exact accepted scope. There is no statement-length cap once the dependency and assumption boundary is explicit.

If the composition needs a real hypothesis, state it and use the interpretive layer rather than rejecting an otherwise useful conditional theorem. A missing bridge is “not yet proved,” not a refutation of either accepted atom.

If the scientific mechanism is genuinely open, compare plausible mechanisms under preregistered structural criteria. If the theorem statement is fixed, declare target_kind: fixed_theorem and proceed with one sound proof route; do not invent rival mechanisms to satisfy a form.

Run scripts/find_synthesis_candidates.py when cross-sector graph structure can help discovery. Treat its ranking as a hint, never as evidence or a gate.

Prove the glue

Choose the strongest practical proof backend for the exact statement:

• Use SymPy for exact identities, substitutions, eliminations, and finite symbolic chains.
• Use Lean for finite formal statements and prioritize an end-to-end theorem over disconnected attestations. Import shared framework definitions where practical, reject proof escapes, inspect the theorem and axiom footprint, and audit the map back to the physics statement.