4  Writing Executables (ExPrograms)

4.1 Assembling Executable Logic

The ExPrograms directory acts as the final deployment target for verified logic within the Lean 4 laboratory. Programs written here structurally demonstrate the topological bounds functioning in real-time.

To write a functional program within ExPrograms, a developer combines the abstract logic structures generated in CombLib and binds them to the execution engine’s structural constraints.

---

4.2 Simulating Execution

Because Lean 4 is utilized as the static oracle prior to hardware deployment, these programs execute by simulating the recursive topological cost that an Interaction Net backend will eventually process natively.

The framework provides specific wrapper functions to trace the execution path of complex logic.

#| label: execute-holographic
#| eval: false

def executeHolographicSweep : Comb :=
  app (Comb.terminal "SC_CUT") (app swarmFilter mockSwarm)

In the example above, executeHolographicSweep wraps a combinatorial data-filtering operation inside a structural bound (SC_CUT). This boundary isolates the execution from triggering global cycle detectors, allowing the algorithm to execute an absolute complement search dynamically.

---

4.3 Designing New Programs

When designing new executables (such as the AgenticPlanning or ColliderSimulation algorithms), developers follow these standard integration steps:

• Initialize Variables: Import the base math primitives from CombLib.
• Establish Bounds: Identify the areas where semantic recursion occurs. Wrap these regions utilizing the engine’s Strongly Cantorian fixpoint evaluators or manual \(T\)-injections.
• Execute and Trace: Map the result to an IO wrapper (like execute_agent_loop) to observe the final topological distance generated by the logic compilation.