Cosmology Rung Descent Unit Step Shift Down Top Unit Step

The unit-step invariant

A graded system assigns a whole-number level, or rung, to each of its parts. In the Recognition Science framework, the parts are cells and the rungs are integers. The framework's central ledger, a discrete record of events, demands that any two connected cells differ by at most one rung. This requirement, called the unit-step invariant, keeps the system from making abrupt jumps.

The question is what happens when the system must relax, lowering some cells by one rung. A naive move, lowering any chosen set, can break the invariant. A concrete counterexample in the framework's machine-checked library of formal theorems shows this: on a chain of three cells with rungs 0, 1, and 2, lowering the bottom cell to -1 makes its gap to the middle cell equal to 2, violating the rule. The generic move is unsafe.

The theorem shiftDown_top_unitStep identifies the one safe move. If a system has a highest rung, and you lower exactly the cells at that top rung, the invariant is preserved. The proof 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 move, both meet at the new level, and the gap is zero. The descent always exists, with no external parameter, because the highest rung is read off the field itself.

In Recognition Science, this result matters because the framework's cost law, which sets the price of recognition, applies only when the unit-step invariant holds. The theorem guarantees that the natural relaxation move, lowering the top rung, keeps the cost law valid for the next cycle. It is the positive half of an honest answer: the generic move fails, but the forced top-rung descent succeeds.

The theorem does not claim that any descent preserves the invariant, nor that the top-rung move is the only possible relaxation. It does not say that the real-valued mean move, which the framework's Phase 58 examined, preserves unit-step; that move fails globally. The result is specific to the integer rung field and the top-rung descent, and it is proved with zero axioms beyond the standard three of the underlying logic.

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

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

What this page does not claim

This theorem does not claim that any descent preserves the unit-step invariant. This theorem does not claim that the real-valued mean move preserves the invariant. This theorem does not claim that the top-rung descent is the only possible relaxation move.

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: