Cosmology Rung Descent Unit Step T59 Rung Descent Preservation

The safe descent

In the Recognition Science framework, a ledger is a discrete record of events, and one of its basic objects is a field of integer rungs assigned to each cell. A rung is just a level number, like a floor in a building. The framework's dynamics moves these rungs, and a central invariant, called unit-step, demands that any two cells connected by an edge differ by at most one rung. The question is whether a particular move, lowering a whole set of cells by exactly one rung, keeps that invariant intact from one cycle to the next.

The answer, proved as a theorem in the framework's machine-checked library of formal theorems, is precise. Lowering an arbitrary set of cells preserves the unit-step invariant exactly when every edge crossing the boundary of that set still has its two endpoints within one rung after the move. Edges entirely inside or entirely outside the lowered set are safe automatically, because both endpoints shift together or not at all. This is the integer analogue of a known negative result about real-valued moves, which fail to preserve the invariant globally.

The theorem then shows a special case that needs no extra condition: if the set being lowered is exactly the set of cells at the top rung, the move always preserves the invariant. The reason is forced. A top-rung cell's neighbor cannot be above it, and the invariant forbids it being two below, so the neighbor must sit exactly one rung down. After the descent, both endpoints meet at the same level, and the gap is zero. This top-rung descent is the natural relaxation move, requiring no externally supplied parameter, and it provably keeps the cost law applicable for the next cycle.

The theorem also includes a counterexample showing the restriction is necessary. On a three-site chain with rungs 0, 1, 2, lowering the bottom cell sends it to -1, making its gap to the neighbor 2, which breaks the invariant. So descending a non-top cell is unsafe. The headline theorem bundles both facts: the top-rung descent always works, and the bottom-rung descent on that chain always fails.

What this does not claim is broader. It does not claim that all dynamics preserve the unit-step invariant, only this specific top-rung descent. It does not claim anything about real-valued moves, which are handled separately and negatively. And it does not claim that the invariant holds for arbitrary sets without the cut condition, which the counterexample refutes.

/-- **Local preservation criterion.** Descending a set `S` by one rung preserves `UnitStep` on the
whole edge set provided every *cut* edge (exactly one endpoint in `S`) remains within one rung
after the move. Edges with both endpoints in `S` keep their gap (both shift by `1`); edges with
neither endpoint in `S` are unchanged. So only the cut edges can break the invariant, and the
hypothesis controls exactly those. -/
theorem shiftDown_unitStep_of_cut (S : V → Prop) [DecidablePred S] (k : V → ℤ)
    (E : Finset (V × V)) (hunit : UnitStep k E)
    (hcut : ∀ p ∈ E, ((S p.1 ∧ ¬ S p.2) ∨ (¬ S p.1 ∧ S p.2)) →
        (shiftDown S k p.1 - shiftDown S k p.2 = 0
          ∨ shiftDown S k p.1 - shiftDown S k p.2 = 1
          ∨ shiftDown S k p.1 - shiftDown S k p.2 = -1)) :
    UnitStep (shiftDown S k) E := by
  intro p hp
  by_cases h1 : S p.1 <;> by_cases h2 : S p.2
  · -- both endpoints descend: the gap is unchanged
    rw [shiftDown_pos S k h1, shiftDown_pos S k h2]
    have hsame : (k p.1 - 1) - (k p.2 - 1) = k p.1 - k p.2 := by ring
    rw [hsame]; exact hunit p hp
  · -- cut edge: p.1 descends, p.2 stays
    exact hcut p hp (Or.inl ⟨h1, h2⟩)
  · -- cut edge: p.1 stays, p.2 descends
    exact hcut p hp (Or.inr ⟨h1, h2⟩)
  · -- neither endpoint descends: unchanged
    rw [shiftDown_neg S k h1, shiftDown_neg S k h2]; exact hunit p hp

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

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

What this page does not claim

The theorem does not claim that all dynamics preserve the unit-step invariant, only this specific top-rung descent. The theorem does not claim anything about real-valued moves, which are handled separately and negatively. The theorem does not claim that the invariant holds for arbitrary sets without the cut condition.

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: