← All posts
science#irdme#topology-as-logic#coq#formal-methods#proof-assistants#preregistration

H_LOGIC_COQ_STDLIB_v1: First Cross-Proof-Assistant Directional Replication

The Coq Corelib replication (n=17) produced a positive directional result consistent with Lean/mathlib4: degree r=0.2875 (positive, p=0.2874), with cross-layer analysis showing moderate persistence (r=0.4913) and betweenness persistence r=0.5091. This is an underpowered but important independent formal-systems replication.

pre-reg: ae32f0092ec03a70…

Why this experiment mattered

H_LOGIC_EXTRACTION on Lean/mathlib4 was strong (r=0.777), but still one proof-assistant corpus.

The scientific question was straightforward: does the signal transfer to an independent formal system?

H_LOGIC_COQ_STDLIB_v1 is that replication on Coq Corelib.

Dataset and protocol

  • Corpus: Coq standard library (Corelib + Ltac2 aggregate)
  • Nodes: 17 top-level modules
  • Layers:
  • require_dependency (module import structure)
  • git_co_development (module co-change in commit history)
  • Git window: depth-2000 history clone
  • Pre-registered before analysis
  • Pre-registration hash: ae32f0092ec03a703f991814d7641f94a095c7e0e36298add94f433545d0ac26
  • Timestamp: 2026-05-30T15:17:36Z

    • Results

    h1 (primary): PARTIAL (direction confirmed)

  • Pearson r = 0.2875 (positive)
  • Spearman r = 0.2721
  • Permutation p = 0.2874
  • n = 17

    • Interpretation: direction is correct but below the pre-registered threshold and underpowered at this sample size.

    h3 (divergence): CONFIRMED

  • 11 of 17 modules showed substantial rank divergence
  • Strong role specialization signal persists

    • h2

    h2 returned ERROR because the test block missed required fields (layer_a, layer_b, expected_hub). It is excluded from inference.

    Note added 2026-05-30: h2 is excluded due to missing required fields in the test block (layer_a, layer_b, expected_hub). This is a protocol implementation gap, not a data issue. The pre-registration hash and timestamp are unaffected. h2 will be re-specified in the next Coq run.

    Cross-layer structure (important context)

      From cross-layer analysis:
    • Hub persistence (degree): r = 0.4913
    • Betweenness persistence: r = 0.5091
    • Persistent hubs in both layers: Corelib.Classes, Corelib.Floats, Corelib.Strings, Corelib.ssr

    This is directionally aligned with the Topology-as-Logic formal-systems claim and supports moving from “single corpus” to “two corpus, one underpowered.”

    Honest interpretation

    This is not a headline statistical confirmation yet. It is a directional replication with limited power.

    That is still meaningful: we now have an independent proof-assistant corpus with non-negative structural transfer and strong divergence signatures.

    The right next step is scale: larger Coq ecosystem datasets (MathComp / coq-community) or deeper history windows.

    IRDME project: arXiv:2604.23639 Public pre-registrations: https://github.com/vladi160/preregistrations

    Reproducibility

    This result was pre-registered before analysis. SHA-256 hash: ae32f0092ec03a703f991814d7641f94a095c7e0e36298add94f433545d0ac26

    Verify at github.com/vladi160/preregistrations