Encyclopedia Cosmology Cosmology Refine Trigger Jcost Arbitrarily Small Positive

ARTICLE 3 claims 3 theorems

Cosmology Refine Trigger Jcost Arbitrarily Small Positive

A rule for refining a coarse simulation into a fine one cannot use any positive tolerance, because a forced change can cost as little as one pleases.

Verify this page

The zero threshold

In a simulation that builds a fine-grained picture from a coarse one, a refiner must decide which regions to refine (split into finer detail). A naive rule descends wherever some measure of activity exceeds a chosen tolerance ε. The Recognition Science framework asks whether that tolerance is a free parameter or something the mathematics forces. Its answer, proved in a machine-checked library of formal theorems, is that the tolerance must be exactly zero.

The framework's recognition cost, a number that measures how much a distinction costs to record, is J(x) = (x + x⁻¹)/2 − 1 for a positive ratio x. A ratio of one, meaning no distinction, costs zero. A ratio away from one costs a positive amount. The theorem jcost_arbitrarily_small_positive states that for every positive ε, no matter how small, there exists a ratio above one whose cost is positive but below ε. In plain terms, a forced distinction can be made arbitrarily cheap, so any positive threshold will eventually skip a distinction that the mathematics requires.

The consequence is structural. The framework proves that lossless reconstruction, rebuilding the fine cell exactly, forces the refiner to descend exactly the blocks that carry an internal posting, a recorded event that must be split. Descending those and only those is lossless, and any lossless decision must include them. A rule that descends only when demand exceeds a positive ε will, by the arbitrarily-small-positive theorem, miss some active block and lose information. Zero is therefore the unique law-given threshold, with no knob to choose.

This result does not say that the recognition cost itself is small in any absolute sense, nor that the framework's refinement rule is the only possible one. It says that if losslessness is the requirement, the threshold is forced. The framework's claim is about the threshold, not about the magnitude of any particular cost, and not about whether refinement is always necessary. A reader can now see why a tuned tolerance is not merely inconvenient but provably unsafe under the framework's own definition of lossless reconstruction.

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 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 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

This does not claim that the recognition cost is small in any absolute sense. This does not claim that the framework's refinement rule is the only possible refinement rule. This does not claim that refinement is always necessary.

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