Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.RungDescentUnitStep

show as:
view Lean formalization →

Defines the integer unit-step rung descent on a graded phi-rung field: every cell in a selected set S drops by exactly one rung, all other cells stay fixed. Cosmology and T-3 refinement arguments cite this as the discrete single-rung move, never a real-valued mean shift. The module builds the shift maps, positivity/negativity cases, edge-vertex bookkeeping, and an existence lemma for a top-cell unit descent.

claimOn a graded $\phi$-rung field, the unit descent $\mathrm{shiftDown}(S)$ lowers every cell in a finite set $S$ by exactly one rung and leaves the complement unchanged; $\mathrm{shiftUp}(S)$ is the inverse raise. The construction yields a genuine unit step (rung change $\pm 1$), edge-vertex membership for the cut, and existence of a top-cell descent realizing that unit step.

background

Recognition Science carries spatial regions on a graded $\phi$-rung profile rather than a single binary sign. The north-star rule is to hold each region at the coarsest rung its recognition budget allows. Upstream, GradedRungCost lifts the binary birth-field ledger (carried bulk free; interface pays count times $J(\phi)$) to this multi-valued rung field: any unit-step $\phi$-rung configuration still pays $J(\phi)$ per forced distinction.

This module supplies the elementary discrete move used by the T-3 refiner: select a cell set $S$ and drop every rung index in $S$ by exactly one integer step. The complementary raise is recorded for bookkeeping. No continuous averaging of rungs appears; the change is always $\pm 1$ on the selected support.

Notation follows the graded ledger: rung values live on the $\phi$-ladder, $J$ is the unique cost $J(x)=(x+x^{-1})/2-1$, and unit steps are the generators whose cost the graded law prices.

proof idea

Definition-first module. It introduces shiftDown and shiftUp as pointwise integer updates on the rung field, then records elementary sign/support lemmas (shiftDown_pos, shiftDown_neg, and the up variants). Cut-local unit-step identities (shiftDown_unitStep_of_cut, shiftDown_top_unitStep) connect the global shift to the graded unit-step predicate from the cost ledger. Edge-vertex helpers (edgeVerts and membership) track the interface of the moved set. The capstone is an existence statement that some top cell admits a unit descent, assembling the local shift facts rather than a deep analytic argument.

why it matters in Recognition Science

Unit rung descent is the atomic move the T-3 refiner posts when it coarsens or refines a graded profile one rung at a time. Without a verified integer step, cost comparisons in GradedRungCost would mix discrete ledger terms with ad-hoc real means. The module therefore sits between the graded cost law and any cosmology argument that walks a rung configuration down (or up) while preserving the $J(\phi)$-per-distinction accounting.

In the broader forcing picture, rungs live on the $\phi$-ladder fixed at T6; single-rung moves keep the ledger aligned with that discrete skeleton. Downstream use is not yet wired in this graph snapshot (used_by empty), but the sibling existence lemma is the natural hook for refinement or descent theorems that need a concrete top-cell unit step.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (18)