Encyclopedia Cosmology Cosmology Rung Descent Unit Step

ARTICLE 4 claims 4 theorems

Cosmology Rung Descent Unit Step

A machine-checked proof shows that the only safe way to relax a graded structure is to lower its top level by exactly one step.

Verify this page

The forced one-rung move

A rung is an integer label attached to a cell in a discrete structure, and a unit-step field is one where every edge connects cells whose labels differ by at most one. The classical question is simple: if you lower a set of cells by one rung, does the field stay unit-step? The answer is no in general, and yes for exactly one kind of move. On a three-site chain with rungs 0, 1, 2, lowering the bottom cell sends it to -1, so its edge to the rung-1 neighbour now has gap 2 and the invariant fails. That failure is not a bug in a particular example; it is a theorem that any such non-top descent breaks the property.

The safe move is to descend the top rung. If every rung in the edge set is at most M, and you lower every cell at rung M by exactly one, the field provably remains unit-step. The reason is forced: a top-rung cell's neighbour cannot be above it, and the unit-step condition forbids it being two below, so the neighbour sits exactly one rung down. After the descent the two endpoints meet at M - 1 and the gap is 0. This is the integer analogue of an earlier result about real-valued moves, but with a key difference: the real-valued mean move does not preserve unit-step globally, while the integer top-rung descent does, unconditionally.

In Recognition Science, the framework models a cost meter that charges each recognition event. The live engine does not move rungs by real means; it descends a region by exactly one rung when a distinction is forced. The module RungDescentUnitStep closes the question of whether that update keeps the unit-step invariant cycle to cycle. It proves that a preserving descent always exists, with no externally supplied parameter: take M to be the realised maximum rung, descend the top cells, and the invariant holds. The dual move, raising the bottom rung, works by symmetry. The cost law from an earlier phase therefore applies to the next cycle, and the meter is theorem-backed along that update.

The necessity counterexample is not cosmetic. On the chain 0, 1, 2, descending the bottom cell breaks unit-step, so the top-rung restriction is essential, not a convenient assumption. The bundled headline theorem states both halves at once: the top-rung descent preserves the invariant for any unit-step field with a rung upper bound, and the concrete chain shows a non-top descent breaks it. Together with the earlier real-valued result, this is the complete, honest answer to whether the dynamics preserves the graded-rung invariant: the generic move does not, but the forced top-rung descent does.

What this changes is practical. A relaxation step that only ever lowers the highest occupied rung is safe by construction, so the engine can run such steps without re-checking the invariant. The proof is machine-checked: the library's theorems carry no axioms beyond the standard three logical postulates, and the counterexample is decided by computation. The reader can now see why a natural relaxation move is the one that preserves structure, and why any other descent is provably unsafe.

THEOREM shiftDown_top_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean
shiftDown_top_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean:105 
/-- **Top-rung descent preserves `UnitStep` unconditionally.** If `M` bounds every rung present in
`E` and `S` is the set of cells at rung `M`, then descending `S` by one rung keeps the field
unit-step. The cut argument is forced: a top-rung cell's neighbour cannot be above it, and
`UnitStep` forbids it being two below, so the neighbour sits exactly one rung down; after the
descent the two endpoints meet at rung `M - 1` and the cut gap is `0`. -/
theorem shiftDown_top_unitStep (k : V → ℤ) (E : Finset (V × V)) (M : ℤ)
    (hunit : UnitStep k E) (hub : ∀ p ∈ E, k p.1 ≤ M ∧ k p.2 ≤ M) :
    UnitStep (shiftDown (fun v => k v = M) k) E := by
  apply shiftDown_unitStep_of_cut (fun v => k v = M) k E hunit
  intro p hp hcut
  obtain ⟨hub1, hub2⟩ := hub p hp
  have hstep := hunit p hp
  rcases hcut with ⟨h1, h2⟩ | ⟨h1, h2⟩
  · -- k p.1 = M (in S), k p.2 ≠ M (out): neighbour is forced to M - 1
    have hb2 : k p.2 < M := lt_of_le_of_ne hub2 h2
    have hk2 : k p.2 = M - 1 := by omega
    have v1 : shiftDown (fun v => k v = M) k p.1 = k p.1 - 1 := shiftDown_pos _ k h1
    have v2 : shiftDown (fun v => k v = M) k p.2 = k p.2 := shiftDown_neg _ k h2
    left; rw [v1, v2]; omega
  · -- k p.1 ≠ M (out), k p.2 = M (in): symmetric
    have hb1 : k p.1 < M := lt_of_le_of_ne hub1 h1
    have hk1 : k p.1 = M - 1 := by omega
    have v1 : shiftDown (fun v => k v = M) k p.1 = k p.1 := shiftDown_neg _ k h1
    have v2 : shiftDown (fun v => k v = M) k p.2 = k p.2 - 1 := shiftDown_pos _ k h2
    left; rw [v1, v2]; omega
THEOREM ckLevels_descend_min_breaks · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean
ckLevels_descend_min_breaks · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean:206 
/-- **Necessity counterexample.** Descending the *bottom* cell (rung `0`) of the chain `0, 1, 2`
sends it to `-1`, so the edge to the rung-`1` neighbour has gap `2` and `UnitStep` fails. Only
descending the top rung is safe; the top-rung hypothesis of `shiftDown_top_unitStep` is necessary,
not cosmetic. -/
theorem ckLevels_descend_min_breaks :
    ¬ UnitStep (shiftDown (fun v => v = (0 : Fin 3)) ckLevels) ckEdges := by
  unfold UnitStep; decide
THEOREM exists_top_descent_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean
exists_top_descent_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean:143 
/-- **A preserving descent always exists.** For any nonempty edge set carrying a unit-step rung
field, take `M` to be the realised maximum rung; descending the top-rung cells preserves
`UnitStep`, and the descent is nontrivial because the maximum is attained. No external parameter
is supplied: `M` is read off the field. -/
theorem exists_top_descent_unitStep [DecidableEq V] (k : V → ℤ) (E : Finset (V × V))
    (hne : E.Nonempty) (hunit : UnitStep k E) :
    ∃ M : ℤ, (∃ v ∈ edgeVerts E, k v = M)
      ∧ UnitStep (shiftDown (fun v => k v = M) k) E := by
  have hVne : (edgeVerts E).Nonempty := by
    obtain ⟨p, hp⟩ := hne
    exact ⟨p.1, fst_mem_edgeVerts hp⟩
  have hImgNe : ((edgeVerts E).image k).Nonempty := hVne.image k
  set M : ℤ := ((edgeVerts E).image k).max' hImgNe with hM
  have hMmem : M ∈ (edgeVerts E).image k := Finset.max'_mem _ hImgNe
  obtain ⟨v, hv, hvk⟩ := Finset.mem_image.mp hMmem
  refine ⟨M, ⟨v, hv, hvk⟩, ?_⟩
  apply shiftDown_top_unitStep k E M hunit
  intro p hp
  refine ⟨?_, ?_⟩
  · exact Finset.le_max' _ (k p.1) (Finset.mem_image.mpr ⟨p.1, fst_mem_edgeVerts hp, rfl⟩)
  · exact Finset.le_max' _ (k p.2) (Finset.mem_image.mpr ⟨p.2, snd_mem_edgeVerts hp, rfl⟩)
THEOREM shiftUp_bot_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean
shiftUp_bot_unitStep · IndisputableMonolith/Cosmology/RungDescentUnitStep.lean:167 
/-- **Bottom-rung raise preserves `UnitStep` unconditionally** (dual of `shiftDown_top_unitStep`).
If `m` bounds every rung from below and `S` is the set of cells at rung `m`, raising `S` by one
rung keeps the field unit-step: a bottom cell's neighbour is forced to be exactly one rung up, so
after the raise the cut gap is `0`. -/
theorem shiftUp_bot_unitStep (k : V → ℤ) (E : Finset (V × V)) (m : ℤ)
    (hunit : UnitStep k E) (hlb : ∀ p ∈ E, m ≤ k p.1 ∧ m ≤ k p.2) :
    UnitStep (shiftUp (fun v => k v = m) k) E := by
  intro p hp
  obtain ⟨hlb1, hlb2⟩ := hlb p hp
  have hstep := hunit p hp
  by_cases h1 : k p.1 = m <;> by_cases h2 : k p.2 = m
  · rw [shiftUp_pos _ k h1, shiftUp_pos _ k h2]
    have hsame : (k p.1 + 1) - (k p.2 + 1) = k p.1 - k p.2 := by ring
    rw [hsame]; exact hstep
  · -- k p.1 = m (raised), k p.2 ≠ m: neighbour forced to m + 1
    have hb2 : m < k p.2 := lt_of_le_of_ne hlb2 (Ne.symm h2)
    have hk2 : k p.2 = m + 1 := by omega
    rw [shiftUp_pos _ k h1, shiftUp_neg _ k h2]
    left; omega
  · -- k p.2 = m (raised), k p.1 ≠ m: symmetric
    have hb1 : m < k p.1 := lt_of_le_of_ne hlb1 (Ne.symm h1)
    have hk1 : k p.1 = m + 1 := by omega
    rw [shiftUp_neg _ k h1, shiftUp_pos _ k h2]
    left; omega
  · rw [shiftUp_neg _ k h1, shiftUp_neg _ k h2]; exact hstep

What this page does not claim

This does not claim that the real-valued mean move preserves unit-step; the opposite is proved. This does not claim that any descent preserves the invariant; only the top-rung descent is safe. This does not claim that the rung field is the only structure the cost meter charges.

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/RungDescentUnitStep.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