feat(types): wire backend consumers + fix z3 build + outcome module

[hyperpolymath]

Step 3 of the native type-system plan: wire backends to consume TypeInfo decorations, extend GNN graph awareness, and fix a pre-existing build break.

Changes:

1. Fix pre-existing z3 build break:

   • Create src/rust/provers/outcome.rs with ProverOutcome enum (8 variants: Proved, InconsistentPremises, NoProofFound, UnsupportedFeature, InvalidInput, Timeout, ProverError, SystemError)
   • Move orphan check method from impl ProverBackend for Z3Backend to its own impl Z3Backend block — it was not a trait member
   • Result: cargo check --lib now passes cleanly (0 errors, 0 warnings)

2. Idris2 QTT multiplicity wiring:

   • export() now reads Definition.type_info.multiplicity and emits QTT annotations (0 , 1 , or unrestricted) on type signatures
   • Added multiplicity_to_idris2() helper mapping all Multiplicity variants to Idris2 QTT syntax
   • Removed duplicate local Multiplicity enum (now uses crate::types)

3. F* effect + refinement wiring:

   • to_input_format() now reads Definition.type_info.effects and emits F* effect prefixes (Tot, IO, ST, Exn, Div, GTot, ALL, Custom)
   • Reads type_info.refinement and emits {v:T | P} syntax
   • Added effect_to_fstar() helper

4. Dedukti exchange layer Sigma support:

   • term_to_dedukti() renders Term::Sigma as dk_sigma A (x => B)
   • parse_dedukti_term() parses dk_sigma back to Term::Sigma

5. GNN graph type-info awareness:

   • Added EdgeKind::HasMultiplicity, HasEffect, HasModality
   • add_type_info_edges() creates annotation nodes and edges from hypothesis/definition type_info decorations
   • Embeddings: added "sigma" label detection in feature extraction, updated quantifier feature to include sigma binders

Test results: 587 passed, 0 failed, 0 clippy warnings.

https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq

[chatgpt-codex-connector]

Codex usage limits have been reached for code reviews. Please check with the admins of this repo to increase the limits by adding credits.
Credits must be used to enable repository wide code reviews.