obtain-immediate-conclusions

name	obtain-immediate-conclusions
description	Derive immediate mathematical consequences from a theorem statement or subgoal. Use when starting a new problem, branch, or subgoal, or when cheap progress or a cleaner reformulation is needed before deeper proof search.

Obtain Immediate Conclusions

Extract direct implications before speculative reasoning.

Input Contract

Read from memory and current context:

• problem_id
• current theorem/subgoal statement
• memory

Procedure

1. Normalize notation and restate the claim in equivalent forms.
2. List direct consequences that follow from definitions and basic algebraic/logical manipulations.
3. Split consequences into necessary conditions and candidate sufficient conditions.
4. Mark each consequence with confidence and justification type.
5. For every conclusion, explicitly decide whether it is likely fragile and should be stress-tested by counterexample.
6. If a conclusion is fragile, record why it is fragile and indicate that $construct-counterexamples should be considered next.

Output Contract

Publish each conclusion to global memory with gm_add (kind conclusion): claim = the conclusion's statement, evidence = the derivation/justification that makes it checkable, and carry these fields in the record:

{
  "statement": "...",
  "justification_type": "by_definition|calculation|known_fact|logical_equivalence",
  "confidence": 0.0,
  "is_fragile": false,
  "fragility_reason": "",
  "suggested_followup": "none|construct-counterexamples",
  "scope": "global|branch|subgoal",
  "branch_id": "optional",
  "subgoal_id": "optional"
}

Rules:

• is_fragile must always be present.
• If is_fragile=true, then fragility_reason must explain the risk and suggested_followup should be construct-counterexamples.
• If is_fragile=false, use fragility_reason="" and suggested_followup="none".

Tools

• gm_add (publish the conclusion finding)
• gm_search (recall related findings across the swarm)
• search_arxiv_theorems for nontrivial consequences
• Codex built-in web search for background definitions/terminology

Failure Logging

If no meaningful consequence is found, note it in your local memory (events) with:

• event_type="immediate_conclusions_stalled"
• missing assumptions and suspected blockers