Positive integer frames for the compact released regions

import Definitions.Def_mme_released_recursive_stage_data
import Definitions.Def_mme_released_joint_interior_frame
import Definitions.Def_mme_graded_integer_regional_step_data
import Mathlib.Tactic.NormNum

set_option autoImplicit false

open scoped BigOperators
open MME MME.RecursiveYZ MME.RegionRealization MME.CompleteSplit
open MME.MoreAsymmetryExactSeed

namespace MME.ReleasedPositiveInteger

/-- Integer geometry over abstract profiles. Keeping these functions as
parameters avoids generating record eliminators over the released tables. -/
structure FrameData {half ell R M B L : ℕ}
    (parent : Fin R → Fin 3 → ℕ) (n : Fin R → ℕ)
    (total : ∀ r, parent r 0 + parent r 1 + parent r 2 = 2 * half)
    (m : ∀ r, RecursiveThinSplit.Split half (parent r) → ℕ)
    (mu : Fin 3 → Cell half R parent → CompleteWord ell → ℕ)
    (length : L * 2 ^ (ell - 1) = M) (minimum : ℕ)
    (grading : ProfiledCW.Predicate M) (source : ℝ → ProfiledCW.Predicate M) where
  hashPositions : Fin (B - 1 + 1) ≃ (r : Fin R) × Fin (n r)
  positions : Fin L ≃ Position n
  reference : RecursiveXHash.Address half R parent n
  reference_target : reference ∈ RecursiveXHash.target m
  mass : ∀ i c, (∑ w, mu i c w) = m c.1 c.2 + m c.1 (complement (total c.1) c.2)
  support : ∀ i c w, 0 < mu i c w →
    ∑ h, (w h).val = (c.2.val i).val
  boundary : BoundaryProfiles mu
  parent_size : ∀ r, minimum ≤ n r
  split_divisible : ∀ r c, minimum ∣ m r c
  parent_graded : ∀ i x,
    ParentGraded parent n i (ProfiledCW.split positions length x) ↔ grading i x
  typical : ∀ (eta : ℝ), 0 < eta → ∀ i x,
    parentTypical total n m (mu i) eta (ProfiledCW.split positions length x) ↔ source eta i x

/-- Construct an integer step without changing the finite geometry. -/
noncomputable def FrameData.step {half ell R M B L : ℕ}
    {parent : Fin R → Fin 3 → ℕ} {n : Fin R → ℕ}
    {total : ∀ r, parent r 0 + parent r 1 + parent r 2 = 2 * half}
    {m : ∀ r, RecursiveThinSplit.Split half (parent r) → ℕ}
    {mu : Fin 3 → Cell half R parent → CompleteWord ell → ℕ}
    {length : L * 2 ^ (ell - 1) = M} {minimum : ℕ}
    {grading : ProfiledCW.Predicate M} {source : ℝ → ProfiledCW.Predicate M}
    (frame : FrameData (B := B) parent n total m mu length minimum grading source)
    (half_eq : half = 2 * 2 ^ (ell - 1)) (minimum_pos : 0 < minimum)
    (repairScale : ℕ) (hrepair : 1 < repairScale)
    (epsilon : ℝ) (hepsilon : 0 < epsilon)
    (hsize : (8 * repairScale : ℝ) *
      (25 * R * (Fintype.card (CompleteWord ell) : ℝ) ^ 2) ≤
        (minimum : ℝ) * epsilon ^ 2) : IntegerStep ell M (source epsilon) where
  half := half
  R := R
  parent := parent
  n := n
  total := total
  half_eq := half_eq
  m := m
  N := B - 1
  hashPositions := frame.hashPositions
  L := L
  positions := frame.positions
  length := length
  mu := mu
  mass := frame.mass
  support := frame.support
  boundary := frame.boundary
  reference := frame.reference
  reference_target := frame.reference_target
  minimum := minimum
  repairScale := repairScale
  minimum_pos := minimum_pos
  repairScale_gt_one := hrepair
  parent_size := frame.parent_size
  split_divisible := frame.split_divisible
  epsilon := epsilon
  epsilon_pos := hepsilon
  size_test := hsize
  source_inside := fun i x hx => (frame.typical epsilon hepsilon i x).mp hx

/-- The compact released specialization keeps all data functions literal.
Its reference is fixed across every step constructed from the frame. -/
abbrev Frame (region : Fin 6) (k : ℕ) :=
  FrameData (half := 4) (ell := 2) (R := 88)
    (M := ReleasedJointInterior.blocks region k * 4)
    (B := ReleasedJointInterior.blocks region k)
    (L := ReleasedJointInterior.blocks region k * 2)
    (RecStage.parent3 region) (fun r => k * RecStage.n3 region r) (RecStage.htotal3 region)
    (fun r c => k * RecStage.m3 region r c) (fun i c w => k * RecStage.mu3 region i c w)
    (ReleasedJointInterior.positions_length region k) (k * denominator ^ 2)
    (fun i x => ParentGraded (ReleasedJointInterior.parent region)
      (ReleasedJointInterior.size region k) i
      (ProfiledCW.split (ell := 2) (ReleasedJointInterior.positions region k)
        (ReleasedJointInterior.positions_length region k) x))
    (ReleasedJointInterior.source region k)

/-- Construct the central integer step with its geometry and profiles unchanged.
The scalar size test is explicit; no copy-rate bound is assumed. -/
noncomputable def Frame.step {region : Fin 6} {k : ℕ}
    (frame : Frame region k) (hk : 0 < k)
    (repairScale : ℕ) (hrepair : 1 < repairScale)
    (epsilon : ℝ) (hepsilon : 0 < epsilon)
    (hsize : (8 * repairScale : ℝ) *
      (25 * 88 * (Fintype.card (CompleteWord 2) : ℝ) ^ 2) ≤
        (k * denominator ^ 2 : ℕ) * epsilon ^ 2) :
    IntegerStep 2 (ReleasedJointInterior.blocks region k * 4)
      (ReleasedJointInterior.source region k epsilon) :=
  FrameData.step frame (by norm_num) (Nat.mul_pos hk (by norm_num [denominator]))
    repairScale hrepair epsilon hepsilon hsize

end MME.ReleasedPositiveInteger