← All papers
First page of Topology as Logic: Structural Role Geometry Across Formal, Software, Biological, and Prebiotic Systems

Topology as Logic: Structural Role Geometry Across Formal, Software, Biological, and Prebiotic Systems

Vladi Ivanov

cs.SI Jun 1, 2026 · v1
Uses the Lean 4 mathlib4 dependency graph as a proof-assistant corpus for network hub-persistence analysis.
We ask whether dependency topology correlates with functional load-bearing organization as recoverable geometry -- not as a metaphor, but as a measurable structural property detectable by multilayer network analysis. Across seven independent substrates, we show that hub persistence and rank divergence under the Functional Proximity Law recover operational organization that domain experts describe as logic: axiomatic load-bearing structure in formal mathematics, control and contract structure in legacy software, conserved hub grammar across approx. 600 million years of neural evolution, catalytic role organization in a published prebiotic autocatalytic network, carry-path dominance in a 4-bit digital circuit, betweenness persistence in the ISCAS85 c432 standard benchmark (n=196), and a directional formal-systems replication in the Coq Corelib (n=17). A key methodological finding: degree-based hub persistence is weak between physical wiring and simulation state-correlation layers (r=0.21 in c432), while betweenness-based persistence is stronger (r=0.77 in the 4-bit ALU post-hoc; r=0.34 in c432). The ISCAS85 pre-registered primary hypothesis was CONFIRMED (degree r=0.426, p=0.002, Spearman r=0.551). The formal-systems claim is supported by two proof-assistant corpora: Lean 4 mathlib4 (CONFIRMED, r=0.777, p=0.004) and Coq Corelib (PARTIAL, direction confirmed, r=0.288, p=0.287, n=17, underpowered). All seven experiments were pre-registered before analysis.

It is unclear whether dependency graph topology can quantitatively recover what domain experts identify as the operational logic of a system, as opposed to merely correlating with it metaphorically. Prior work lacked a systematic cross-domain empirical test.

The authors apply the IRDME multilayer network framework and the Functional Proximity Law across seven substrates: two digital circuits, two formal proof corpora (Lean 4 mathlib4 and Coq Corelib), legacy COBOL software, cross-species neural connectomics, and a prebiotic autocatalytic network. All hypotheses were pre-registered before analysis. Hub persistence and rank divergence are measured using both degree-based and betweenness-based centrality across structural layers. The Lean 4 mathlib4 analysis confirms strong cross-layer hub correlation (r=0.777, p=0.004).

All seven pre-registered experiments show positive hub persistence. The primary methodological finding is that betweenness-based persistence (r=0.771 in the 4-bit ALU) dominates degree-based persistence in detecting load-bearing logic nodes. The ISCAS85 c432 benchmark confirmed the degree hypothesis (r=0.426, p=0.002, Spearman r=0.551). The Coq replication was directionally consistent but underpowered (r=0.288, n=17).

SubstratenPrimary metricFinding
Digital (4-bit)29Betweenness r=0.771 (post-hoc); degree r=0.512, p=0.004CONFIRMED
Digital (c432)196degree r=0.426, p=0.002, Spearman r=0.551CONFIRMED
Formal (Lean)20Pearson r=0.777, Spearman r=0.733, p=0.004CONFIRMED
Formal (Coq)17degree r=0.288, p=0.287PARTIAL
Legacy SW (COBOL)14r=0.807, p=0.002CONFIRMED
Neural (cross-species)2952cosine>=0.90CONFIRMED
Prebiotic1 networkcatalytic hubCONFIRMED
Seven-substrate evidence base