R8 BitNB CN* rank-count packs (densified cND)

Definition

IntMul_Kappa_R8_Data_BitOppbankGenCN

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

bitnbintmulkapparound8

Rank-count packs `CN1_` / `CN2_`

cntF of densified genF segment chunks. Node ids remapped to $0..nNodes-1$ ( $nNodes=62478$ ) so cND stays below codeBound=64251 (R6 isND used $38286$ ).

Definition code

import Mathlib.Data.Nat.Basic

set_option autoImplicit false
set_option relaxedAutoImplicit false

/-!
# R8 opp-bank CN* rank packs (densified cND)

Node ids densified to `0 .. 62477`; `codeBound = 1773 + nNodes = 64251`.
-/

namespace IntMul.Kappa.R8.Bit.Oppbank.GenCN

def nNodes : ℕ := 62478
theorem nNodes_eq : nNodes = 62478 := rfl

/-- Rank-count pack `CN1_0`. -/
def CN1_0 : ℕ := 0

/-- Rank-count pack `CN1_1`. -/
def CN1_1 : ℕ := 7606387081216

/-- Rank-count pack `CN1_2`. -/
def CN1_2 : ℕ := 55808805046126

/-- Rank-count pack `CN1_3`. -/
def CN1_3 : ℕ := 168901881785973771409367274299306216702056534074276018869729942912263215568780089525678354751052489266655318970768602727151327515054601651852028596763777167919079645955958324625422683806

/-- Rank-count pack `CN1_4`. -/
def CN1_4 : ℕ := 31937084640975886314307985140717147638313451778475849278494628151054563607017791006608655722746875743030490749445621121099625533144021590448500117257710457103757693296658642433648961798503667036

/-- Rank-count pack `CN1_5`. -/
def CN1_5 : ℕ := 118623462721834333714207366003601528855833786467865295191229796848093924537016547775352697881052842576171863267545352866474883348364481122439214589093587145981163039901667590095405293446595876603

/-- Rank-count pack `CN1_6`. -/
def CN1_6 : ℕ := 155952509220275631690979608803871153591432212772412147050782886605793958366005062649227720027558801326061842498726927707600856739398979021939930863746274570398700167516414791867446129000049300536876544402747086077965

/-- Rank-count pack `CN1_7`. -/
def CN1_7 : ℕ := 2824194695642645963992122392163592482489722342619352801782484697079381884648382156959914452253096300385992117250287667530996850421154532588919701815682940710988194207051075321585466367820088066625644736642799310782036122271744

/-- Rank-count pack `CN1_8`. -/
def CN1_8 : ℕ := 0

/-- Rank-count pack `CN1_9`. -/
def CN1_9 : ℕ := 149051210906274711701180689321291325867034428652797454482743287669355594324162082175412854971961746353967789405508665977116118632241208266265589759341191695764331217945095606134358984243410168516599365581185101070336

/-- Rank-count pack `CN1_10`. -/
def CN1_10 : ℕ := 0

/-- Rank-count pack `CN2_0`. -/
def CN2_0 : ℕ := 0

/-- Rank-count pack `CN2_1`. -/
def CN2_1 : ℕ := 0

/-- Rank-count pack `CN2_2`. -/
def CN2_2 : ℕ := 152922670929814314602510057875091100564879478747675310443334022414014181189724733660488513542662051454070848870586813145352900934377343545908851844573244653678055589041537845882633620361418665223368113419332391801611

/-- Rank-count pack `CN2_3`. -/
def CN2_3 : ℕ := 34873586608168428075601575474895176540990581766560104878509736736975954424164215012497417073714394497276066715495244400539726338652898251629000087185248346761900468004762689282

/-- Rank-count pack `CN2_4`. -/
def CN2_4 : ℕ := 87838130361782749065758054070503072742611023643379367882967853488540380725720741828222153297518727462212694945983582288589207818143853371191280125420046067330785534886256617848544409724932486982363637610691287344468797165667

/-- Rank-count pack `CN2_5`. -/
def CN2_5 : ℕ := 2736356565434879994134870168333554894821614297320262737160435580184046875035599582566919045724369781992165858897928163497300810584550902232269264970842261502900394762629980612487420205774681302602155491153894768094086839664640

/-- Rank-count pack `CN2_6`. -/
def CN2_6 : ℕ := 0

/-- Rank-count pack `CN2_7`. -/
def CN2_7 : ℕ := 0

/-- Rank-count pack `CN2_8`. -/
def CN2_8 : ℕ := 0

/-- Rank-count pack `CN2_9`. -/
def CN2_9 : ℕ := 0

end IntMul.Kappa.R8.Bit.Oppbank.GenCN

Source

Python port of Defs51.cntF/dimCF over densified grec_full.pkl

View graph

R8 BitNB CN* rank-count packs (densified cND)

Rank-count packs CN1_* / CN2_*

Rank-count packs `CN1_` / `CN2_`