Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2026
|
| Online Access: | https://doi.org/10.5281/zenodo.19897980 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Table of Contents:
- <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]">We introduce <em>Coherence Debt</em>, a quantitative measure of the propositional coherence obligations accumulated by categorical formalizations that achieve kernel rigidity via a non-univalent universe (Mechanism 3 in our taxonomy). We define the <em>Fording Density</em> δ = N_bridge/N_term and the <em>Weighted Coherence Debt</em> WCD as predictors of elaboration overhead in Lean 4. We then apply the ALoTT Coherence Debt Engine to <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">HoTTLean.Groupoids.FunctorOperation.refl</code>, the sorry-free reflexivity construction in Nawrocki et al.'s groupoid model of homotopy type theory (CPP 2026). The audit detects five <code class="bg-text-200/5 border border-0.5 border-border-300 text-danger-000 whitespace-pre-wrap rounded-[0.4rem] px-1 py-px text-[0.9rem]">CategoryTheory.Discrete.eqToHom</code> bridge sites at depths 6–10, constituting a nonzero <em>Monodromy Residual</em>: a sequence of context-dependent propositional transports whose endpoints diverge under non-trivial monodromy in the base groupoid. This confirms that the sorry-free construction incurs Coherence Debt at depths far exceeding the shallow-bridge regime, and that the weak-pullback identity elimination semantics of Nawrocki et al. does not eliminate path-dependent bridging for n ≥ 1 categories. We state the precise repair conditions, connect the findings to open obligations in the ALoTT program, and provide an executable audit pipeline for future library maintainers.</p> <p class="font-claude-response-body break-words whitespace-normal leading-[1.7]"><strong>Keywords:</strong> coherence debt, fording density, monodromy residual, categorical proof assistants, Lean 4, Mathlib, HoTTLean, natural model semantics, identity types, rigidity.</p>