Component · spec & evidence

Target Shape Tactic Routing Gate

Records an allow-or-reject decision and reason for each proof tactic before any proof runs.

Contract

Does Before a proof is attempted, this component checks a list of candidate proof tactics for a given goal and writes down an allow-or-reject decision, with a plain reason, for each one. Rejections fall into three kinds: the tactic isn't actually available in the declared environment, it was never listed in the environment's tested set of tactics, or it simply doesn't fit the kind of goal being proved. The resulting record shows, tactic by tactic, exactly what was admitted or blocked and why, instead of an opaque "we tried these" claim. It only inspects and records the routing decision over references that already exist; it never runs a prover or proves anything itself.

Scope limit It only inspects and records the projection mechanics of pre-execution tactic-routing references — emitting per-tactic allow/reject decisions with reasons. It does not run Lean/Lake, does not establish or judge the correctness of any goal, emits no proof bodies, makes no external model access, performs no post-execution route selection, reports no benchmark claims or maturity, and excludes launch.

Run

PYTHONPATH=src python3 -m microcosm_core.cli target-shape-tactic-routing-gate run-routing-bundle --input examples/target_shape_tactic_routing_gate/exported_target_shape_tactic_routing_bundle --out receipts/runtime_shell/demo_project/organs/target_shape_tactic_routing_gate

Evidence

ClassComputed projectionevidence 3/5Source-faithful refactor

Links to Formal Math Verifier Trace Repair Loop, Formal Evidence Cell Anchor Resolver, Proof Diagnostic Evidence Spine, Tactic Portfolio Availability Probe, Verifier Lab Kernel

formal-methodstheorem-provinglean

Source

Source Design note · Source

Map Show on the map

Index Open compact index card

Paper module