Same Domain, Different Answer: What Layer Choice Reveals About Formal Mathematics

The Puzzle

The original mathematics experiment (BC3) denied the Functional Proximity Law:
• r(formal_containment ↔ proof_usage) = +0.105
• r(formal_containment ↔ naming) = +0.280
• Δr = −0.175 → DENIED

The prediction was that set-membership containment and proof usage, both structural mathematical relations, should align more than either does with naming. They don't.

When a prediction fails, IRDME reports a named boundary condition rather than treating it as noise. The BC3 mechanism was: layer resolution mismatch — formal containment encodes atomic, single-level set membership; proof usage creates holistic long-range dependencies that cross formal boundaries. The two layers operate at different abstraction levels.

The Follow-up Test (F9)

If the BC3 denial is about resolution mismatch and not about mathematics itself, then a different layer pair — one without the resolution mismatch — should confirm the law in the same domain.

That is exactly what F9 tested.

Dataset: 20 top-level modules from Lean 4 mathlib4 — the formal mathematics library for the Lean proof assistant.

Layers:
• import_graph (d1): which modules import which — a declared structural dependency layer
• proof_co_development (d3): which modules are co-modified in the same commit with τ ≥ 5 commits — a behavioral co-development layer

Both layers are at the same granularity (module-to-module). No resolution mismatch.

Pre-registered prediction (hash 4ffcdac5, committed 2026-05-20): import_graph ↔ proof_co_development should be more correlated than either is with a dissimilar layer.

The Result

r(import_graph ↔ proof_co_development) = +0.777 (Spearman = 0.733, p = 0.002)

Confirmed. h1 CONFIRMED, h2 CONFIRMED. h3 PARTIAL: Algebra and Analysis swap ranks (Algebra is the top import hub; Analysis is slightly higher in co-development), but the overall pattern holds.

What This Isolates

The comparison between BC3 and F9 is a controlled natural experiment:

| | BC3 | F9 | |---|---|---| | Domain | Formal mathematics | Formal mathematics | | Dataset | 20 abstract mathematical concepts | 20 Lean 4 mathlib4 modules | | Layer pair | formal_containment ↔ proof_usage | import_graph ↔ proof_co_dev | | Resolution | Mismatched (atomic vs holistic) | Matched (module-level, both) | | Result | DENIED | CONFIRMED |

The only variable that changed is the layer pair (and the specific dataset, which is a different implementation of the same domain). The denial localises to the layer choice, not to mathematics as a domain.

This is exactly what the boundary condition framework predicts: the law holds when both layers are at the same structural resolution. BC3 failed that condition; F9 satisfies it.

Why This Matters

Structural science is only useful if it can distinguish why something fails. "Mathematics denies the law" is a dead end. "The formal-containment/proof-usage pair denies the law because of resolution mismatch, but the import/co-development pair confirms it" is a refining statement.

It means: if you want to find hub modules in a mathematical library using the Functional Proximity Law, use module-level layers (imports, co-development). If you use atomic set membership vs holistic proof traversal, the law does not apply — by known mechanism, not by failure.

Pre-registration Record

Hash: 4ffcdac5… — committed 2026-05-20 UTC. Full record: github.com/vladi160/preregistrations (commit 6d6d657).

Paper: arXiv:2604.23639