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.