IndisputableMonolith.Cosmology.RungDescentUnitStep
Defines the integer single-rung descent (and ascent) operators on a graded phi-rung field: every cell in a designated set S drops by exactly one rung, all other cells stay fixed. Cosmology and T-3 refinement arguments cite these maps as the discrete move that never averages rungs over reals. The module builds the operators, positivity/negativity lemmas, edge-vertex bookkeeping, and an existence result for a top-cell unit-step descent.
claimOn a graded rung field $r$, the unit-step descent $\mathrm{shiftDown}(S,r)$ sends every site $x\in S$ to $r(x)-1$ and leaves $x\notin S$ unchanged; $\mathrm{shiftUp}$ is the opposite integer lift. The module records sign lemmas, the fact that a cut-supported descent is a genuine unit step, edge-vertex membership for the support graph, and existence of a top-cell unit-step descent.
background
Recognition Cosmology carries a multi-valued phi-rung profile rather than a single binary charge. The upstream graded-rung cost ledger (GradedRungCost) states that any unit-step phi-rung field pays $J(\varphi)$ per forced distinction, generalizing the binary birth-interface cost of Phase 55.
The present module supplies the elementary discrete dynamics that ledger expects: an integer move that changes selected rungs by exactly $1$. The doc-comment frames this as the single-rung move the T-3 refiner posts; it is deliberately not a real-valued mean or fractional rung shift.
Notation: $S$ is the active cell set; $r$ is the rung assignment; edge vertices track the combinatorial support of the cut across which the unit step is charged.
proof idea
Definition-heavy module with short supporting lemmas. shiftDown and shiftUp are pointwise integer updates on $S$. Sign lemmas (shiftDown_pos, shiftDown_neg, and the up variants) discharge by case split on membership in $S$ and the sign of the original rung. shiftDown_unitStep_of_cut and shiftDown_top_unitStep identify when the support is a genuine unit cut. edgeVerts with fst_mem_edgeVerts / snd_mem_edgeVerts are membership facts for the cut graph. exists_top_descent_unitStep assembles those pieces into an existence claim for a top-cell descent.
why it matters in Recognition Science
Gives the discrete rung motion that the graded cost law meters: without a clean unit-step operator, the $J(\varphi)$-per-distinction ledger has nothing to charge. In the broader RS chain this sits under cosmology / T-3 refinement, where regions must be carried at the coarsest admissible phi-rung and then stepped by integers only (primer: phi-ladder mass formula, T6 phi fixed point). No downstream Lean consumers are wired yet in the graph; the module is infrastructure for later descent-cost and refiner theorems that will quote the unit-step maps and the top-descent existence result.
scope and limits
- Does not prove the graded cost identity; that lives in GradedRungCost.
- Does not allow fractional or real-mean rung updates, only integer $\pm 1$ on $S$.
- Does not derive physical mass, redshift, or observational cosmology claims.
- Does not yet connect to a named parent theorem in the used-by graph.
- Does not address multi-rung jumps or simultaneous updates of overlapping cuts.
depends on (1)
declarations in this module (18)
-
def
shiftDown -
def
shiftUp -
lemma
shiftDown_pos -
lemma
shiftDown_neg -
lemma
shiftUp_pos -
lemma
shiftUp_neg -
theorem
shiftDown_unitStep_of_cut -
theorem
shiftDown_top_unitStep -
def
edgeVerts -
lemma
fst_mem_edgeVerts -
lemma
snd_mem_edgeVerts -
theorem
exists_top_descent_unitStep -
theorem
shiftUp_bot_unitStep -
def
ckLevels -
def
ckEdges -
theorem
ckLevels_unitStep -
theorem
ckLevels_descend_min_breaks -
theorem
t59_rung_descent_preservation