Hub-and-Spoke Orchestration: The Perqed v3.0 Architecture

The evolution of Perqed from a formal verification wrapper into an autonomous hypothesis engine necessitated a fundamental architectural shift. The current implementation utilizes a Hub-and-Spoke model to facilitate interdisciplinary synthesis and rigorous empirical falsification.

Architectural Topology: The Hub-and-Spoke Model

In the v3.0 architecture, the Architect serves as the central orchestration hub, coordinating specialized spokes to ingest literature, formulate hypotheses, and execute computational validation. This decoupling ensures that strategic planning is isolated from the specific mechanics of empirical search or formal proof.

The Librarian Spoke provides grounding by retrieving structurally diverse academic literature from a local vector store (LanceDB). This enables the Architect to synthesize conjectures by pairing techniques from conceptually distant domains—for instance, applying spectral graph theory invariants to solve discrete coloring problems.

The Falsification Pipeline: Empirical Rigor

To maintain mathematical integrity, Perqed prioritizes falsification over verification. Conjectures are subjected to an automated multi-stage evaluation loop before any formal proof is attempted:

1. Sandboxed Empirical Execution: The Explorer Spoke generates and executes probing scripts within isolated environments. These environments are pre-configured with a comprehensive suite of mathematical libraries, including SymPy, SciPy, NetworkX, and Z3.
2. Automated Self-Correction: If an empirical test fails due to implementation errors, the spoke performs a diagnostic analysis of the traceback, refines the test logic, and re-executes. This loop ensures that falsification is based on mathematical truth rather than transient execution errors.
3. Dynamic Skill Injection: The system utilizes a Domain Affinity Mapper to inject relevant mathematical "skills"—formalized representations of proof techniques—into the active spoke's context. This minimizes context pollution and focuses the model on the most appropriate strategic frameworks.

Falsification as a Strategic Priority

The engine's primary objective is the rapid identification of counter-examples. If a hypothesis is contradicted by empirical evidence—such as a specific graph identified as a counter-example via a Python script—the system immediately discards the conjecture. This "fail-fast" approach ensures that the high-latency formal verification spoke (Lean 4) is reserved exclusively for high-confidence conjectures.

By integrating empirical search, literature grounding, and formal verification within a unified Hub-and-Spoke framework, Perqed achieves a level of autonomous mathematical discovery that exceeds simple search-based methodologies.