>_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

⊢⊣⊢⊣

>_MENTAT.JOIN

“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

Ethics, review & quality assurance

Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS

>_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