Cosmology Refine Trigger

/-- **The descent set is forced.** Refining only the blocks in `D` is lossless if and
only if `D` covers every block that carries an internal posting. There is no tunable
slack: lossless reconstruction requires descending exactly the active blocks. -/
theorem lossless_iff (block : ℕ → ℕ) (D : ℕ → Prop) [DecidablePred D] (m : Multiset Event) :
    reconstructUnder block D m = m ↔ ∀ e ∈ internalOf block m, D (block e.source) := by
  unfold reconstructUnder
  rw [← Multiset.filter_eq_self]
  constructor
  · intro h
    have h2 : crossOf block m + (internalOf block m).filter (fun e => D (block e.source))
            = crossOf block m + internalOf block m := by
      rw [h]; exact (cross_add_internal block m).symm
    exact add_left_cancel h2
  · intro h
    rw [h]
    exact cross_add_internal block m

/-- **The law-given rule is lossless.** Descending exactly the active blocks
reconstructs the cell with zero loss. -/
theorem lossless_law (block : ℕ → ℕ) (m : Multiset Event) :
    reconstructUnder block (descendLaw block m) m = m := by
  rw [lossless_iff]
  intro e he
  exact Multiset.mem_map.mpr ⟨e, he, rfl⟩

/-- **The law-given rule is minimal.** Any lossless decision must descend every active
block; you cannot skip a block that carries a posting. -/
theorem descendLaw_necessary (block : ℕ → ℕ) (D : ℕ → Prop) [DecidablePred D]
    (m : Multiset Event) (h : reconstructUnder block D m = m) :
    ∀ b, descendLaw block m b → D b := by
  intro b hb
  obtain ⟨e, he, hbe⟩ := Multiset.mem_map.mp hb
  have hD := (lossless_iff block D m).mp h e he
  rwa [hbe] at hD

/-- **Forced postings have arbitrarily small positive cost.** For every `ε > 0` there is
a ratio above one whose recognition cost is positive but below `ε`. This is why no
positive threshold is safe: a forced distinction can sit just under any `ε`. -/
theorem jcost_arbitrarily_small_positive (ε : ℝ) (hε : 0 < ε) :
    ∃ x : ℝ, 1 < x ∧ 0 < Jcost x ∧ Jcost x < ε := by
  have hδpos : 0 < min 1 ε := lt_min (by norm_num) hε
  have hδ1 : min 1 ε ≤ 1 := min_le_left _ _
  have hδε : min 1 ε ≤ ε := min_le_right _ _
  have hx1 : (1 : ℝ) < 1 + min 1 ε := by linarith
  have hpos : (0 : ℝ) < 1 + min 1 ε := by linarith
  have hne0 : (1 + min 1 ε) ≠ 0 := hpos.ne'
  refine ⟨1 + min 1 ε, hx1, jcost_pos hpos hx1.ne', ?_⟩
  have key : Jcost (1 + min 1 ε) = (min 1 ε) ^ 2 / (2 * (1 + min 1 ε)) := by
    unfold Jcost; field_simp; ring
  rw [key, div_lt_iff₀ (by nlinarith : (0 : ℝ) < 2 * (1 + min 1 ε))]
  nlinarith [hδpos, hδ1, hδε, hε,
    mul_nonneg hδpos.le (by linarith : (0 : ℝ) ≤ 1 - min 1 ε), mul_pos hε hδpos]

/-- **No positive threshold is safe.** For every `ε > 0` there is a cell with a single
internal posting whose demand is positive but below `ε`. The threshold rule "descend
iff demand exceeds `ε`" therefore skips that active block, and the reconstruction is
lossy. Only the zero threshold (descend iff a distinction is forced) is law-given. -/
theorem epsilon_unsafe (ε : ℝ) (hε : 0 < ε) :
    ∃ (m : Multiset Event) (b : ℕ),
      0 < demand b01 m b ∧ demand b01 m b < ε
      ∧ reconstructUnder b01 (fun c => ε < demand b01 m c) m ≠ m := by
  obtain ⟨r, hr1, hrpos, hrlt⟩ := jcost_arbitrarily_small_positive ε hε
  refine ⟨{(⟨0, 1, r⟩ : Event)}, 0, ?_, ?_, ?_⟩
  · -- demand b01 {⟨0,1,r⟩} 0 = Jcost r
    have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
      unfold demand internalOf
      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
    rw [hd]; exact hrpos
  · have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
      unfold demand internalOf
      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
    rw [hd]; exact hrlt
  · -- the epsilon-rule skips block 0, so reconstruction drops the only posting
    have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
      unfold demand internalOf
      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
    have hnotsel : ¬ (ε < demand b01 {(⟨0, 1, r⟩ : Event)} 0) := by rw [hd]; linarith
    -- reconstructUnder = crossOf (empty) + internal filtered by a false predicate = 0
    have hrecon : reconstructUnder b01 (fun c => ε < demand b01 {(⟨0, 1, r⟩ : Event)} c)
        {(⟨0, 1, r⟩ : Event)} = 0 := by
      unfold reconstructUnder crossOf internalOf
      simp [sameBlock, b01, Multiset.filter_singleton, hnotsel]
    rw [hrecon]
    -- 0 ≠ {⟨0,1,r⟩}
    intro hcontra
    have : Multiset.card (0 : Multiset Event) = Multiset.card {(⟨0, 1, r⟩ : Event)} :=
      congrArg Multiset.card hcontra
    simp at this