R8 densified net0P is RunsOK and EdgesOK/FormalOK for large primes

Open

IntMul.Kappa.R8.Bit.Oppbank.net0_ok

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

bitnbinteger-multiplicationkappanet0-okoppbankr8

Let $\mathrm{net0P}$ be the densified opp-bank QH-network of width $m=529$ on $W=104719230$ roles (published Net0P, with honest Pnd ND projectors available via BitOppbankPnd). There exists a bound $q_0$ such that $\mathrm{RunsOK}(\mathrm{net0P})$ holds, and for every prime $q>q_0$ and every $f$ , both $\mathrm{EdgesOK}$ and $\mathrm{FormalOK}$ hold at the prime power $q^f$ .

The RunsOK half is already proved in GoodPrimes via a finite edge family $E_0$ and EdgeQ. The remaining half is the Defs52 good_primes retarget at $\mathrm{codeBound}=64251$ , using NetFB Lab0 certificates and densified Pnd/HasCentre.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs4
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankNet0P
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankGoodPrimes
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankNetFB
import Definitions.Def_IntMul_Kappa_R8_Data_BitOppbankPnd
import Mathlib

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa.R8.Bit.Oppbank

open IntMul.Kappa.R6.Bit
open IntMul.Kappa.R6.Bit.QHNet (RunsOK EdgesOK FormalOK)
open IntMul.Kappa.R8.Bit.Oppbank.Net0P

/-- Densified opp-bank network `net0P` is RunsOK and EdgesOK/FormalOK above a prime bound. -/
theorem net0_ok :
    ∃ q₀ : ℕ,
      RunsOK (m := 529) net0P ∧
        (∀ q, q.Prime → q₀ < q → ∀ f,
          EdgesOK (m := 529) net0P (q ^ f) ∧ FormalOK (m := 529) net0P (q ^ f)) := by
  sorry

end IntMul.Kappa.R8.Bit.Oppbank

Source

GoodPrimes fac3e30f; NetFB cb08d016; Pnd 1351eb81; Net0P 373d80bb; Defs52 net0_ok

View graph