Topology Is Logic: H_LOGIC_EXTRACTION Confirmed 4/4

The Claim

H_LOGIC_EXTRACTION asks a direct question: can we read operational logic from structure alone?

Not symbolic translation. Not post-hoc labeling. Structural role geometry itself.

Pre-registered Setup

Dataset: Lean4 mathlib4 multilayer graph.
• d1: import_graph (declared logical dependency)
• d3: proof_co_development (behavioral proof construction coupling from co-change)

Pre-registered hash: bc2fd106... Date: 2026-05-27

Result

4/4 CONFIRMED
• h1 CONFIRMED: strong cross-layer hub persistence
• Pearson r=0.777
• Spearman=0.7328
• p=0.004
• h2 CONFIRMED: Algebra is #1 in d1 (import_graph)
• h3 CONFIRMED: Analysis is #1 in d3 (proof_co_development)
• h4 CONFIRMED: 3 high-divergence modules (rank_gap>=8):
• CategoryTheory
• Combinatorics
• Order

Why this matters

This is not just another law replication.

F9 showed that formal mathematics still follows IRDME structural persistence. H_LOGIC_EXTRACTION goes one step further: the pattern of hubs and divergences maps to distinct functional roles in the proof ecosystem.
• Convergence hubs in d1 encode axiomatic dependency concentration
• Convergence hubs in d3 encode operational proof traffic concentration
• Divergent modules encode role shifts between declared structure and active construction practice

In short: logic-role geometry is measurable.

What changed after this run

This result upgrades the "Topology as Logic" direction from framing to evidence. It now has a pre-registered empirical anchor, not only theory.

The next step is external replication beyond Lean4: same test structure on additional formal proof corpora and non-math logical systems.

---

IRDME project: arXiv:2604.23639 All pre-registrations are public in the preregistrations repository.