Encyclopedia Cosmology Cosmology Refine Trigger Descend Law Necessary

ARTICLE 4 claims 4 theorems

Cosmology Refine Trigger Descend Law Necessary

When a simulation must preserve every detail of a coarse cell, the rule for which blocks to refine is forced: you cannot skip a block that carries an internal posting.

Verify this page

The necessary descent

In computational cosmology, refining a coarse simulation cell means expanding its hidden internal structure. A naive refiner descends wherever some measure exceeds a tuned tolerance, an epsilon chosen by the programmer. The Recognition Science framework's ledger, a discrete record of events, removes that choice. The theorem descendLaw_necessary states a necessity: if a decision about which blocks to refine reconstructs the fine cell with zero loss, then that decision must include every block that carries an internal posting. You cannot skip a block with active internal structure and still claim lossless reconstruction.

The proof is short and structural. Reconstruction under a decision D is lossless exactly when D covers every block that has an internal posting, a fact the framework proves as lossless_iff. The law-given rule, descend exactly where a posting is forced, is itself lossless, and any lossless decision must contain it. The theorem descendLaw_necessary is the minimality half: it says no lossless decision can omit an active block. The threshold is therefore zero, read off the ledger, with no epsilon to tune.

Why zero is the only safe threshold follows from a separate result. A forced posting can have arbitrarily small positive recognition cost, measured by J(x) = (x + x⁻¹)/2 - 1. For any positive epsilon, there exists a cell with an active block whose demand is below that epsilon. A rule that descends only when demand exceeds epsilon would skip that block and lose information. Zero is unique: descend iff a distinction is forced.

In Recognition Science, this is T-3 of the Cosmogenesis engine, a machine-checked result with no unproved assumptions. The practical consequence is a refiner with no free parameter: the decision to refine is determined by the structure of the ledger itself. What the theorem does not claim is that the physical universe works this way. It proves a property of a formal model, not an empirical fact about cosmology.

THEOREM descendLaw_necessary · IndisputableMonolith/Cosmology/RefineTrigger.lean
descendLaw_necessary · IndisputableMonolith/Cosmology/RefineTrigger.lean:98 
/-- **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
THEOREM lossless_iff · IndisputableMonolith/Cosmology/RefineTrigger.lean
lossless_iff · IndisputableMonolith/Cosmology/RefineTrigger.lean:66 
/-- **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
THEOREM jcost_arbitrarily_small_positive · IndisputableMonolith/Cosmology/RefineTrigger.lean
jcost_arbitrarily_small_positive · IndisputableMonolith/Cosmology/RefineTrigger.lean:125 
/-- **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]
THEOREM epsilon_unsafe · IndisputableMonolith/Cosmology/RefineTrigger.lean
epsilon_unsafe · IndisputableMonolith/Cosmology/RefineTrigger.lean:159 
/-- **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

What this page does not claim

The theorem does not claim that the physical universe refines itself this way. It does not claim that any positive threshold is safe, only that zero is the unique law-given one. It does not claim that the recognition cost function is derived here; that is a separate result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/RefineTrigger.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND