Cost of the Prop 18 descriptor for `n` (round six, `desc18P_cost_g`)
ProvedNLogN.KFM.desc18P_cost_gCost of the Prop 18 descriptor for n.
The following holds (Lean statement, in the scope of module Solutions.R6ZSD):
theorem NLogN.KFM.desc18P_cost_g (dst : Fin HS) (hd : D18Ok dst) {d₀ d₁ r₀ K₀ ℓ₀ b₀ : ℕ} (hb8 : 8 ≤ b₀)
(hd1 : 1 ≤ d₀) (hdb : d₀ ≤ b₀) (hr : r₀ ≤ 2 ^ b₀) (hKd : K₀ ≤ b₀) (hlb : ℓ₀ ≤ b₀)
(hdp : d₁ ≤ d₀) (t : IState HS)
(h : D18G t d₀ d₁ r₀ K₀ ℓ₀ b₀) :
(desc18P dst).cost t ≤ 10 ^ 12 * (b₀ + 1) ^ 3
Context. Round six, chirp: the Prop 18 descriptor for any parameters
The frozen KFMSD.desc18P_run_n / desc18P_cost_n with the values of n (dP n, dpN n, rP n, KP n, ℓP n, bP n) replaced by free values d₀ d₁ r₀ K₀ ℓ₀ b₀ on the registers.
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs16 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open NLogN NLogN.KFM open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP NLogN.RS
theorem NLogN.KFM.desc18P_cost_g (dst : Fin HS) (hd : D18Ok dst) {d₀ d₁ r₀ K₀ ℓ₀ b₀ : ℕ} (hb8 : 8 ≤ b₀)
(hd1 : 1 ≤ d₀) (hdb : d₀ ≤ b₀) (hr : r₀ ≤ 2 ^ b₀) (hKd : K₀ ≤ b₀) (hlb : ℓ₀ ≤ b₀)
(hdp : d₁ ≤ d₀) (t : IState HS)
(h : D18G t d₀ d₁ r₀ K₀ ℓ₀ b₀) :
(desc18P dst).cost t ≤ 10 ^ 12 * (b₀ + 1) ^ 3 := by sorry