YukonModule.ProximityPrize.SubmissionLower.MovingSourceLowZ23Counts6814.part0

import Definitions.Def_Yukon_f53921b9b22d3fcb96996433

import Definitions.Def_Yukon_e35b4a9947b0b30874d0bba4












































































































































































































































































































































































set_option backward.isDefEq.respectTransparency.types false
/-! Kernel-checked dimensions for lower-total Z source 23.
Only the existing closed count/rank formulas are evaluated. -/
namespace ProximityPrize.SubmissionLower.MovingSourceLowZ23Counts6814
open SecondJetRelaxedGlobalIndex SecondJetRelaxedGlobalCounts
set_option autoImplicit false
set_option maxRecDepth 100000
set_option maxHeartbeats 2000000

def cutoff (h : ℕ) : ℕ :=
  114*181255-SecondJetRelaxedDifferentiation.reserve 5 7 h*50186

theorem middle_cap (h : ℕ) (_hh : h≤20) : 155≤(cutoff h+45-1)/131071 := by
  unfold cutoff SecondJetRelaxedDifferentiation.reserve
  split_ifs <;> omega

theorem coefficients_value :
    coefficientCount cutoff 131071 3382 45 20 155=2147578068607419 := by
  decide +kernel

theorem rank_value : SecondJetRelaxedCounts.rankBound 114 3382 45 20 155=8192358200 := by
  decide +kernel

theorem source_card : Fintype.card (Index cutoff 131071 3382 45 20 155)=2147578068607419 := by
  rw [card_index_closed cutoff 131071 3382 45 20 155 (by omega),coefficients_value]

theorem source_rank : SecondJetRelaxedGlobalMap.rankBound 114 3382 45 20 155
    (fun h => (cutoff h+45-1)/131071)=8192358200 := by
  rw [SecondJetRelaxedCounts.rankBound_eq_closed 114 3382 45 20 155 _
    (by omega) (by omega) (by omega) (by omega) middle_cap,rank_value]






end ProximityPrize.SubmissionLower.MovingSourceLowZ23Counts6814