2  Using and Extending CombLib

2.1 The Combinatory Library

The CombLib module provides the native mathematical primitives for the nf-sketches logic engine. Rather than relying on the Calculus of Inductive Constructions, this library implements all mathematical logic entirely via point-free bracket abstraction using the core Comb AST.

By eliminating named variables during execution, the memory architecture avoids the overhead of managing substitution scopes and maps efficiently to parallel GPU evaluation pipelines (e.g. Interaction Nets).

2.2 Transfinite Macro-Primitives

Building upon the Topologically-Guided boundaries established in untyped-comb, the framework implements highly saturated configurations natively via Church Encodings:

  • Core Operators: Node-collision Booleans (and, or, not), B-combinator-based Numerals (succ, add, mult), and inductive Lists geometries via raw bracket abstraction.
  • Recursive Self-Models (\(V \in V\)): The SelfModels.lean primitive constructs a mathematically robust Quine atom (\(\Omega = \{\Omega\}\)) natively inside the engine utilizing the Y-combinator. The architecture evaluates a structure containing an unreduced copy of itself, relying directly on K-Iteration bounds to safely halt the resulting paradox.
  • Choice-Free Cardinal Arithmetic: Implements Transfinite Calculus (e.g., Cardinal Addition \(|A| + |B|\)) via pure bracket abstraction over disjoint union topologies. Operations are bounded structurally across stratification hierarchies using t_inject topological friction markers, completely bypassing the Axiom of Choice.
  • Physical Observables & Particles: By treating graph complexity as thermodynamic friction, we can model physical observables mathematically. Explicitly extracts theoretical physics metrics (Rest Mass, Coupling Constant) from structured particle knots (electron_knot) by measuring bounded topological recursion costs.

2.3 Holographic Data & Search Isolation

Because the engine processes a closed, saturated universe governed by Syntactic Monism, it natively supports operations based on the absolute complement (\(\{x \mid x \notin A\}\)), a construct strictly forbidden in standard ZFC.

The Holographic.lean module operationalizes this complement space. Instead of iterating through data via traditional \(O(N)\) list sweeps, the compiler constructs “exclusion-first” logic gate wrappers. By compiling the query to the complement mapping of the target identity, the framework evaluates a localized topological sweep that filters out non-matching paths in \(O(1)\) time.

Furthermore, by passing distributed data swarms through the \(O(V+E)\) DAG topological sort, the pipeline actively isolates unresolvable contradictions across the entire network in linear time.

2.4 Extending the Library

Developers can contribute to CombLib by defining new Church-encoded structures. When extending the library, algorithms must be written strictly as combinatorial compositions.

Because the engine processes an unstratified universe, developers must account for structural loops natively.

#| label: extending-comblib
#| eval: false

-- Example structure utilizing Schönfinkel primitives
def customCombinator : Comb :=
  app Comb.S (app Comb.K Comb.I)

If an algorithm requires unbounded iteration, the developer must utilize the \(T\)-operator injection (Comb.t_inject) to explicitly mark the recursive topological cost, allowing the underlying geometry constraint solvers to trace the mathematical limits without infinite regress.