construct-proof

name	construct-proof
description	Construct a proof for a framed hypothesis — build lemma chains, import library proofs, seal into a bundle. Use when an engineer needs to prove a specific property.

Construct a proof

You are helping an engineer who has a framed problem (axioms + hypotheses) and needs to construct a proof for ONE specific hypothesis. The framing was done by a domain expert; the proof is your job.

Prove one property at a time. Each sealed bundle maps to one requirement.

Key principle: focused proofs, not monoliths

The framer gave you multiple independent hypotheses. Prove each one separately:

framed_satellite.py:
├── h_stability    → prove → seal → hash_stability    → REQ-STAB
├── h_controllable → prove → seal → hash_controllable → REQ-CTRL
├── h_observable   → prove → seal → hash_observable   → REQ-OBS
└── h_lyapunov     → prove → seal → hash_lyapunov     → REQ-LYAP

Each proof is simple, reviewable, and independently re-verifiable. If the system changes and stability breaks, you re-prove h_stability without touching the controllability proof.

Use import_bundle ONLY when one hypothesis genuinely depends on another (e.g., the proof of uniqueness imports the proof of strict convexity). If they're independent, prove them independently.

Argument

The specific hypothesis to prove: $ARGUMENTS

Workflow

Step 1: Load the framed problem

Read the axioms and the specific hypothesis you're proving. Understand:

• What symbols are involved and their assumptions
• What the hypothesis claims
• Whether it depends on another hypothesis (check the traceability map)

Step 2: Check the library

Before writing custom lemmas, check if a library function covers this directly:

Control: closed_loop_stability, lyapunov_from_system, controllability_rank, observability_rank, hurwitz_second_order, gain_margin, quadratic_invariant

Convex: convex_scalar, convex_hessian, strongly_convex, unique_minimizer, convex_composition, conjugate_function

Physics: constant_acceleration, shm_solution_verify, shm_energy_conservation, work_energy_theorem, gravitational_potential_from_force

Linear Opt: feasible_point, dual_feasible, strong_duality, lp_optimal, integer_feasible

Topology: verify_open, verify_closed, verify_compact, continuous_at_point, intermediate_value, extreme_value

Circuits: gate_truth_table, circuit_equivalence, r1cs_witness_check, boolean_entropy

Information: entropy, mutual_information, kl_divergence, binary_symmetric_channel

DeFi: fee_complement_positive, amm_output_positive, amm_product_nondecreasing

Envelope: envelope_theorem

Core: max_ge_first, piecewise_collapse

If a library function covers the claim, use it. That's what the library is for.

Step 3: Try direct proof

from symproof.tactics import auto_lemma
lemma = auto_lemma("claim", hypothesis.expr, assumptions={...})

If auto_lemma returns a Lemma, you have a one-step proof. Build and seal.

Step 4: Decompose if needed

Common decomposition patterns:

Helper symbol (for bounded intervals):

g = sympy.Symbol("g", positive=True)  # g = 1-f
# Rewrite in terms of g, Q.positive works on all-positive symbols

Algebraic chain (for inequalities):

# Prove (a-b)^2 >= 0, then expand, then rearrange to target form

Import and extend (when this property depends on another):

# Only if the framer flagged a dependency
builder.import_bundle(prior_bundle).lemma("new_step", ...)

Step 5: Build and seal

Always build axiom sets under unevaluated() to prevent SymPy's eager evaluation from collapsing expressions:

from symproof import unevaluated

with unevaluated():
    axioms = AxiomSet(name="system", axioms=(...))

Build and seal:

script = (
    ProofBuilder(axioms, hypothesis.name, name="...", claim="...")
    .lemma("step_1", LemmaKind.EQUALITY, expr=..., expected=...,
           description="why this step matters")
    .build()
)
bundle = seal(axioms, hypothesis, script)

If the axiom set includes expr=True axioms backed by foundation proofs, pass them to seal():

foundation = make_foundation_bundle()
bundle = seal(axioms, hypothesis, script,
              foundations=[(foundation, "theorem_name")])

This enforces that all of the foundation's axioms appear in your axiom set. If they don't, seal() names the hidden axioms. Add them with inherited=True and a Citation:

from symproof import Citation

Axiom(name="missing_condition", expr=condition, inherited=True,
      citation=Citation(source="Theorem source, Author Year"),
      description="Required by theorem_name foundation.")

Always check for hidden axioms when citing external results. This is the most common soundness gap in applied proofs.

Step 6: Report and visualize

Print the traceability record, then render the proof visually so the engineer confirms the math and structure match their intent.

from symproof.export import latex_bundle, proof_dag_mermaid

print(f"Requirement: REQ-STAB")
print(f"Hypothesis:  {hypothesis.name}")
print(f"Status:      {bundle.proof_result.status.value}")
print(f"Hash:        {bundle.bundle_hash}")
print(f"Advisories:  {len(bundle.proof_result.advisories)}")

# Show assumption summary (always present in advisories)
for adv in bundle.proof_result.advisories:
    if "[ASSUMPTIONS]" in adv:
        print(f"  {adv}")

# Show the proof as the reviewer will see it
print("\n--- Proof (LaTeX) ---")
print(latex_bundle(bundle))

# Show the dependency structure
print("\n--- Proof DAG ---")
print("```mermaid")
print(proof_dag_mermaid(bundle))
print("```")

Always show both views. The LaTeX confirms the math (axioms, hypothesis, lemma chain, advisories). The DAG confirms the structure (what depends on what, which bundles are imported). If the engineer says "that's not what I meant," the visual makes the disagreement concrete and actionable.

Step 7: Save

Write a Python file that imports the framed problem, constructs and seals the proof, and prints the traceability record. Runnable standalone.

When you get stuck

1. Check if the axioms are strong enough — the framer may need to add a constraint
2. Try numeric spot-checks — if the hypothesis is false for some parameter values, no proof exists
3. Check known SymPy limitations — the library may have a workaround
4. Report back: "This hypothesis requires axiom X to be provable" or "SymPy cannot verify this expression class"

What you do NOT do

• Do NOT combine multiple independent hypotheses into one proof
• Do NOT weaken the hypothesis to make it easier
• Do NOT change the axioms without consulting the framer
• Do NOT skip advisories — they're part of the deliverable for the auditor