← All posts
science#irdme#topology-as-logic#mathcomp#coq#preregistration#boundary-condition

H_LOGIC_MATHCOMP_v1: h2 Protocol Fixed, Boundary Signal Found

MathComp was run as a pre-registered formal-corpus follow-up with corrected h2 schema fields. Result: h1 DENIED (near-zero cross-layer persistence), h2 PARTIAL, h3 CONFIRMED (role divergence), indicating a boundary-style structural regime rather than a clean persistence replication.

Why this run was necessary

The previous two Topology-as-Logic follow-ups (F3 and Coq Corelib) exposed a protocol issue: h2 test blocks were under-specified and returned ERROR.

    H_LOGIC_MATHCOMP_v1 was designed to do two things at once:
  • Run one more real formal corpus (MathComp).
  • Fix h2 schema properly (layer_a, layer_b, expected_hub) and verify the workflow produces a normal verdict instead of ERROR.

Pre-registration discipline

  • Experiment: H_LOGIC_MATHCOMP_v1
  • Pre-registration hash: fe6b29dd51521fcbc0d8deb7f1c51da32b2e699ef3017866de0a1b3b19bbdf0a
  • Public prereg commit: 3ada0de
  • Prediction verification after run: MATCH (unchanged hypotheses)

    • Dataset

  • Graph: COQ_MATHCOMP_v1
  • Nodes: 9 top-level packages
  • Layers:
  • require_dependency (declared package dependencies)
  • git_co_development (package co-change coupling from git history)
  • Relations: 50 total

    • Results

    | Hypothesis | Verdict | Key evidence | |---|---|---| | h1 | DENIED | Pearson r = -0.0513, p = 0.986 (near-zero/negative persistence) | | h2 | PARTIAL | boot top in require_dependency but not top in git_co_development (field top there) | | h3 | CONFIRMED | 4 packages with rank gap >= 3 |

    What this means

    This is not a clean formal-corpus persistence replication.

      It is still a scientifically useful run because it provides two concrete outputs:
    • Protocol correction confirmed: h2 now executes correctly (no schema ERROR).
    • Boundary-style signal: MathComp shows strong divergence structure without positive hub persistence at this package granularity.

    In plain terms: declared dependency and development co-change are telling different structural stories in this corpus, and IRDME detected that mismatch.

    Honest next step

    The right follow-up is not to force this into a confirmation narrative.

      The right follow-up is a planned boundary experiment family on formal corpora with:
    • larger node sets / finer granularity
    • explicit nulls and rewired baselines
    • pre-registered effect thresholds tied to sample size

    That will separate "true persistence failed" from "resolution/regime mismatch at current granularity".

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