NF Sketches: Documentation

Introduction and Setup

The Acyclic Lean Architecture

The nf-sketches repository provides a computationally verifiable, topologically-bound combinatory logic engine. This documentation guides engineers and researchers through the ecosystem’s theoretical validation matrix.

The primary objective of this architecture is to resolve cyclical logic constraints without relying on external garbage collection, hierarchical universes (like HoTT or ZFC), or global substitution environments. By formalizing Quine’s systemic ambiguity (the idea that sets can shift their typestate dynamically without strict ontological boundaries) into geometric routing rules, the logic engine natively processes highly entangled variables by extracting topological paths directly from the Abstract Syntax Tree (AST).

A Multidisciplinary Convergence

At first glance, this repository may seem to jump between disparate fields. This is intentional. The engine synthesizes four distinct domains into a single computational pipeline:

  1. Proof Theory (Sequents, Natural Deduction): Provides the syntax and logical rules (Quine’s NF) ensuring the math is rigorously sound.
  2. Graph Theory (Bellman-Ford, DAGs): Translates those logical rules into geometric constraints, converting paradoxes into detectable “negative-weight cycles.”
  3. Combinatory Logic (\(S\), \(K\), \(Y\)): Flattens the verified graph into an untyped, variable-free state, perfectly suited for bare-metal and parallel GPU execution.
  4. Theoretical Physics (Observables, Resonance): Acts as the ultimate stress test. By treating unstratified combinatorial loops as thermodynamic systems, we measure the “friction” of logic itself, producing computational analogs to physical knots.

This repository functions as the theoretical laboratory—utilizing Lean’s trusted kernel to formally prove algorithmic stratification, K-Iteration limits, and topological boundaries. It conducts the rigorous diagnostic work required to secure cryptographic certainty before the mathematical concepts are independently forged into custom bare-metal engines (like the Rust-based monist engine).

Practical Setup

The environment is built utilizing Lean 4, which acts as the static verification oracle.

To initialize the operational environment across all sub-modules (nf-validate, parse-strat, seq-embed, and untyped-comb), execute the provided build scripts:

#| label: build-script
#| eval: false

./update-lean.sh
lake build

These commands synchronize the mathematical verification matrices with the exact mathlib cache required for the topological algorithms.

The Workflow Paradigm

The development lifecycle within nf-sketches follows a distinct progression from string parsing to combinatory execution limits:

  1. Interactive Sandbox (parse-strat): Users first define logical constraints using standard ASCII syntax to test stratification boundaries and manually trace Extensionality Collisions.
  2. Static Validation (nf-validate): The logic is converted into constraint algebra, running Bellman-Ford evaluation to intercept topological paradoxes as negative-weight cycles.
  3. Formal Diagnostics (seq-embed): Deep embedding of Sequent Calculus simulating cut-reduction dynamically against comprehension axioms.
  4. Primitive Assembly (CombLib & untyped-comb): Mathematical concepts are assembled via variable-free combinators, bypassing dependent types entirely.
  5. Executable Deployment (ExPrograms): Verified logic structures are deployed as functional scripts that map natively onto Interaction Nets, setting the physical proofs for combinatorial execution algorithms.