[{"hi":[2,1],"keepRight":false,"lo":[1,1],"mid":[3,2],"nativeHi":[2,1],"nativeLo":[1,1],"step":0},{"hi":[3,2],"keepRight":true,"lo":[1,1],"mid":[5,4],"nativeHi":[3,2],"nativeLo":[1,1],"step":1},{"hi":[3,2],"keepRight":true,"lo":[5,4],"mid":[11,8],"nativeHi":[3,2],"nativeLo":[5,4],"step":2},{"hi":[3,2],"keepRight":false,"lo":[11,8],"mid":[23,16],"nativeHi":[3,2],"nativeLo":[11,8],"step":3},{"hi":[23,16],"keepRight":true,"lo":[11,8],"mid":[45,32],"nativeHi":[23,16],"nativeLo":[11,8],"step":4},{"hi":[23,16],"keepRight":false,"lo":[45,32],"mid":[91,64],"nativeHi":[23,16],"nativeLo":[45,32],"step":5},{"hi":[91,64],"keepRight":true,"lo":[45,32],"mid":[181,128],"nativeHi":[91,64],"nativeLo":[45,32],"step":6},{"hi":[91,64],"keepRight":false,"lo":[181,128],"mid":[363,256],"nativeHi":[91,64],"nativeLo":[181,128],"step":7},{"hi":[363,256],"keepRight":false,"lo":[181,128],"mid":[725,512],"nativeHi":[363,256],"nativeLo":[181,128],"step":8},{"hi":[725,512],"keepRight":false,"lo":[181,128],"mid":[1449,1024],"nativeHi":[725,512],"nativeLo":[181,128],"step":9},{"hi":[1449,1024],"keepRight":false,"lo":[181,128],"mid":[2897,2048],"nativeHi":[1449,1024],"nativeLo":[181,128],"step":10},{"hi":[2897,2048],"keepRight":false,"lo":[181,128],"mid":[5793,4096],"nativeHi":[2897,2048],"nativeLo":[181,128],"step":11},{"hi":[5793,4096],"keepRight":true,"lo":[181,128],"mid":[11585,8192],"nativeHi":[5793,4096],"nativeLo":[181,128],"step":12}]
'ActualMathematics.RefinementLesson.refine_nested' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.width_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.precision_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.any_precision' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.value_eq_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.value_irrational' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.nativeRatio_display' depends on axioms: [propext, Classical.choice, Quot.sound]
'ActualMathematics.RefinementLesson.nativeRatio_square' depends on axioms: [propext, Classical.choice, Quot.sound]