3.4.2 Formal status and empirical burden

3.4.2 Formal status and empirical burden

DIAL turns the missing bridge into two linked obligations. The formal obligation is not a single missing lemma. It comprises five tasks:

1. define a category \(\mathbf{DIAL}(\mathcal M)\), including its objects, morphisms, sidewise involution laws, and mixed interchange axiom;

2. prove stability under tangent lift and under the transports required by finite theory extension;

3. establish a realization theorem relating \(\mathbf{DIAL}(\mathbf{Smooth})\) to classical double Lie algebroids, with the required dualizability doctrine stated explicitly;

4. determine whether the resulting objects admit products, pullbacks, representations, cohomology, and integration to an appropriate double groupoid semantics; and

5. internalize the matched-pair description by 2-term representations up to homotopy, prove independence from the chosen splitting, and explain how the two Yang–Baxter-style side laws interact with mixed double coherence.

The last task matters because two valid involution algebroids do not automatically form a DIAL object.

The empirical obligation is to show whether this additional structure earns its keep. A computational DIAL realization must expose two typed repair directions, estimate an interchange witness, localize its support, and test whether the candidate local repair persists as a coherent finite realization. Only then may that information support selection or construction of a finite sketch extension. The complete system must be compared with single-direction tangent repair, untyped two-operator search, fixed-sketch LINCS, and an equally resourced frontier-model proposer. Success means better admitted extensions, not merely a larger obstruction score.

. DIAL is falsifiable at two levels. It can fail mathematically if no coherent internal double construction has the claimed classical realization, and it can fail computationally if its typed interchange information does not improve proposal quality, sample efficiency, localization, or conservative abstention.