substrate-framework: Skill for Codex

Theorem Synthesis

The elite result is a useful new implication, not a restated atom or isolated special value. Apply AGENTS.md and physics-erdos-loop/SKILL.md for the shared reward, supervision, continuation, and promotion contract.

Achievement — identify the missing glue

Read current release, relevant accepted claims and source. Instantiate memory-templates/theorem-synthesis.md and validate its proposal before proof work. State the exact higher theorem, at least two distinct accepted dependencies, structural gap, assumptions/exclusions/consumers, and core or interpretive layer. Audit dependency use against accepted scope; prior acceptance remains intact. An explicit hypothesis earns a useful conditional interpretive theorem. A missing bridge is an open construction, not a refutation of the atoms.

A fixed theorem uses target_kind: fixed_theorem and one sound proof route. When the higher theorem or bridge is still being discovered, use ../physics-discovery/SKILL.md. Complement scripts/find_synthesis_candidates.py and current graph/AST hints with structural correspondences between sectors that have no accepted dependency edge yet. Write the object, field/metric/action map, hypotheses and missing implication before treating a resemblance as glue. Open mechanisms compete under frozen structural criteria; a straightforward fixed proof can proceed without a discovery exercise. The explicit assumption boundary, not a statement-length cap, controls scope.

Achievement — prove the composition

Use SymPy for exact identities, substitutions, elimination, and finite chains. Use Lean where it proves the actual finite statement; prefer an end-to-end theorem using shared definitions. Audit statement, imports, proof escapes, axiom footprint, and physical encoding. Meaningful mutation belongs to custom translators/symbolic/numerical verifiers, not a ceremonial mutation of the kernel. Lean is complementary, not a universal prerequisite.

Keep proof, empirical applicability, and interpretation separate in verification_evidence. Measurements/simulations test nature and consequences; they supply neither the proof of an exact implication nor hidden derivation inputs.