>_PROJECT.NO_COINCIDENCE_CNCC

Computational No-Coincidence
Neyman's CNCC in Lean 4

Extended Research — Eric Neyman (ARC, 2025) | Formalized March 15, 2026

Overview

Eric Neyman (ARC, 2025) conjectures that for reversible circuits on $\{0,1\}^{3n}$ exhibiting a “non-coincidental” zero-suffix property, there exist short advice strings $\pi$ that serve as polynomial-time verifiable structural explanations. This formalization does not prove CNCC itself — it builds a candidate verifier architecture that makes the conjecture's structure explicit.

The key insight: advice strings are naturally modeled as nucleus operators (closed, idempotent, order-preserving maps) on the lattice of circuit properties. This turns the informal notion of “structural explanation” into a formally tractable fixed-point condition. The core theorem ( $\texttt{gap\_characterizes\_soundness}$ ) proves a genuine biconditional: gap = 0 iff all accepted circuits have the target property.

Modules

20

16 source + 4 test

Theorems

56

Machine-verified

Lines

1,037

Proof code

Sorry

0

Zero gaps

Audits

2

Adversarial

>_VERIFICATION.SEAL

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

56 THEOREMS VERIFIED20 MODULES1,037 LINES0 SORRY2 HOSTILE AUDITS

No-Coincidence CNCC • Lean 4 + Mathlib • Apoth3osis Labs

>_PROOF.MODULES

Formal Modules (5 packages, 13 theorems, 941 lines)

>_NEYMAN.CORRESPONDENCE

Neyman ↔ HeytingLean Correspondence

Neyman Concept	Lean 4 Formalization	Module
$reversible circuit on \{0,1\}^{3n}$	Basic.RevCircuit n	Basic/Circuit.lean
$zero-suffix property P(C)$	Basic.PropertyP n C	Basic/Property.lean
$short advice string \pi$	nucleus selector (size, involution, property)	Nucleus/AdviceAsNucleus.lean
$structural explanation$	CircuitNucleus.explains	Nucleus/CircuitNucleus.lean
$executable advice screen$	candidateScreen n C \pi	Nucleus/AdviceAsNucleus.lean
$sound verifier V(C,\pi)$	candidateVerifier n C \pi	Nucleus/AdviceAsNucleus.lean
$soundness slack$	circuitHeytingGap R P	Nucleus/HeytingGapSoundness.lean
$dimensional decomposition$	three canonical lenses	Structure/DimensionalBound.lean
$hierarchical compression$	adviceWeight via WeightSystem.weight	Structure/HierarchicalAdvice.lean
$circuit Heyting consequence$	circuit\_heyting\_gap\_and\_non\_boolean	Bridge/UnificationTheorem.lean
$neural-net interpretability$	NeuralNetAsCircuit + explainedByStructure	Bridge/NeuralNetBridge.lean
$Wolfram parallel$	wolfram\_independence\_parallel	Bridge/UnificationTheorem.lean

>_DEPENDENCY.GRAPH

Module Dependency Graph

Upstream Foundation Core Constraints Consequences Meta

>_PROVENANCE

Provenance Chain

THEORY

Eric Neyman, “Computational No-Coincidence Conjecture,” ARC (Alignment Research Center), 2025

PROOF

Lean 4 formalization by Apoth3osis Labs — 56 theorems, 20 modules, 1,037 lines, 0 sorry

KERNEL

Kernel-checked, twice adversarially audited (initial + remediation re-audit)

BRIDGE

Connected to HeytingLean infrastructure: Hossenfelder no-go boundary, Wolfram confluence-causal invariance, sheaf-neural semantics, Hybrid-Zeckendorf weight system

VIEW ON GITHUB VIEW RESEARCH PAGE

Computational No-CoincidenceNeyman's CNCC in Lean 4