Prove2Me

R8 densSup tip 3_7

Definition
IntMul_Kappa_R8_Data_BitOppbankSupDense3_7

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

bitnbintmulkapparound8

Densified support quarter tip

Assembles densSupT{q} from part packs for densSupG.

Definition code
-- R8 opp-bank densified node supports (jfstack_23, dense d ↔ raw d+1).
-- Generated by notes/track_bitnb/gen/emit_sup_dense_pnd.py

import Definitions.Def_IntMul_Kappa_R6_Defs50
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_0
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_1
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_2
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_3
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_4
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_5
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankSupDense3_6

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option maxRecDepth 100000

namespace R6Chk.Bit

noncomputable def densSupT3_p111 : BT :=
(BT.node
 (BT.node
  (BT.node
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))))
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))))
  (BT.node
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))))
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))))))
 (BT.node
  (BT.node
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))))
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))))
  (BT.node
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))))
   (BT.node
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))
    (BT.node
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0)))
     (BT.node
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))
      (BT.node
       (BT.leaf 0)
       (BT.leaf 0))))))))

/-- densified support subtree 3 (leaves 3072..4095). -/
noncomputable def densSupT3 : BT := (BT.node (BT.node (BT.node densSupT3_p000 densSupT3_p001) (BT.node densSupT3_p010 densSupT3_p011)) (BT.node (BT.node densSupT3_p100 densSupT3_p101) (BT.node densSupT3_p110 densSupT3_p111)))

end R6Chk.Bit
Source
emit_sup_dense_pnd.py / Track A Pnd

View graph