Computational No-Coincidence Conjecture
Formal verification framework for Neyman's CNCC using Heyting algebra nucleus operators as poly-time advice strings for reversible circuit structural explanations.
Theory: Eric Neyman (ARC, 2025) · Formalized: March 15, 2026
Modules
20
16 source + 4 test
Theorems
56
Machine-verified
Lines
1,037
Proof code
Sorry
0
Zero gaps
Audits
2
Adversarial
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.
No-Coincidence CNCC • Lean 4 + Mathlib • Apoth3osis Labs
Can we build a poly-time verifier that checks whether a reversible circuit's behavior has a structural explanation?
Neyman (ARC, 2025) proposes that for reversible circuits on { 0,1 }³ⁿ exhibiting a “non-coincidental” zero-suffix property, short advice strings should exist that serve as polynomial-time verifiable structural explanations. The question is: what mathematical structure do these advice strings have, and can we build a sound verifier for them?
The key discovery: 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.
A nucleus on a Heyting algebra is the right abstraction because it provides exactly the right level of structure: extensive (the explanation covers the circuit), idempotent (applying the explanation twice is the same as once), and meet-preserving (combining two explanations is itself an explanation). The fixed points of the nucleus are precisely the “explained” circuit properties.
This connection also reveals a crucial distinction: heuristic advice screens (which check the property directly) are not sound, while nucleus-based certified verifiers (which check the fixed-point condition) are sound. The formalization makes this distinction explicit and proves it.
Basic
Reversible circuits, zero-suffix property, CNCC statement
Nucleus
Advice as nuclei, gap soundness, fixed-point verifier
Structure
Dimensional bounds, hierarchical advice, reversibility
Bridge
Hossenfelder consequence, neural-net, Wolfram parallel
Meta
Nucleus implication, Boolean-collapse heuristic
Import spine: Basic → Nucleus → Structure → Bridge → Meta
FORMALLY PROVED
- ✓Gap characterizes soundness (biconditional)
- ✓Nucleus construction with all 3 axioms
- ✓Circuit Heyting gap implies non-Booleanity
- ✓Candidate verifier soundness
- ✓Bijectivity of reversible circuit evaluation
REMAINS CONJECTURAL
- ?CNCC itself (whether all P-circuits admit short advice)
- ?Whether the nucleus model captures all structural explanations
- ‖Wolfram confluence parallel (explicit, not formal consequence)
- ‖Neural-net interpretability bridge (conceptual parallel)
Initial adversarial audit of all 20 modules. Identified remediation items in vacuous theorems and definitional aliases. All findings addressed.
Remediation re-audit confirming all findings from Audit 1 were addressed. Zero sorry, zero admit, no remaining vacuous theorems.
“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.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
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.
Contribution Certificates
Immutable contribution records per MENTAT-CA-001. Each certificate is a cryptographically anchored MCR documenting authorship, contribution level, and provenance chain. Artifacts are content-addressed and pinned to IPFS.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerComputational No-Coincidence Conjecture
Contributor
Eric Neyman
ARC (Alignment Research Center)
Core conceptual insight: for reversible circuits exhibiting a non-coincidental zero-suffix property, there should exist short advice strings serving as polynomial-time verifiable structural explanations. The conjecture bridges computational complexity with interpretability by asking whether structure has a formal, verifiable witness.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerMathematical Framework for Circuit Structural Explanations
Contributor
Eric Neyman
ARC (Alignment Research Center)
Complete mathematical framework: reversible circuits as bijections on Fin(2^(3n)), zero-suffix property as a structural invariant, advice strings as short certificates, and the central conjecture that P-circuits always admit poly-time verifiable explanations.
Builds Upon
MENTAT Contribution Record
APPLICATION
Applied Contribution
CONTRIBUTION LEVEL: APPLICATION
Ontological EngineerCNCC as Foundation for Interpretability
Contributor
Eric Neyman
ARC (Alignment Research Center)
Connection from the no-coincidence principle to AI alignment: if structural explanations for circuit behavior can be verified in polynomial time, this provides a formal foundation for understanding why neural networks work, beyond post-hoc rationalization.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization: Nucleus-Based Advice Verification
Contributor
Apoth3osis Labs
R&D Division
Complete Lean 4 formalization: 56 theorems across 16 source + 4 test modules (1,037 lines). Key innovation: encoding advice strings as Heyting algebra nucleus operators (closed, idempotent, order-preserving maps) on the circuit-property lattice. Core result: gap_characterizes_soundness (genuine biconditional — gap=0 iff all accepted circuits have the target property).
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerKernel-Checked Proofs with Adversarial Audit
Contributor
Apoth3osis Labs
R&D Division
All 56 theorems kernel-checked by the Lean 4 type checker. Twice adversarially audited (initial audit + remediation re-audit). Zero sorry, zero admit. IPFS-pinned source archive for permanent, content-addressed verification.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerHeytingLean Infrastructure Bridge
Contributor
Apoth3osis Labs
R&D Division
Production integration connecting the CNCC formalization to existing HeytingLean infrastructure: Core.Nucleus for lattice operations, Hossenfelder no-go boundary for non-Booleanity, Wolfram confluence-causal invariance as parallel structure, Hybrid-Zeckendorf weight system for hierarchical advice, and sheaf-neural semantics for interpretability.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026