Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.RecognitionUnitStepPreservation

show as:
view Lean formalization →

Real-valued Phase-56 unit-step invariant: on a coupling graph, every listed edge has recognition-level gap at most one. Needed because pairResolve averages endpoints and can produce half-rungs from integer inputs. Cosmology and forward-dynamics work cite it to keep graded rung fields inside the unit-step regime where the J-cost ledger applies. Arguments are local gap checks plus short chain examples (three-edge paths).

claimA real-valued rung field $x$ on a finite vertex set is unit-step along a listed edge set $E$ when every edge $\{i,j\}\in E$ satisfies $|x(i)-x(j)|\le 1$. The module records this predicate, the local touching relation for edges under pair-resolve, and proves that if $x$ is unit-step on the edges that touch a resolved pair, then the post-resolve field (both endpoints sent to their mean) remains unit-step on those edges. Explicit three-edge chain examples illustrate preservation through successive mean moves.

background

Recognition equilibrium evolves a field of recognition levels $x:\mathrm{Fin},n\to\mathbb{R}$ on a coupling graph by forced pair-resolve: each tick sends a coupled pair to their mean (the $\sigma=0$, $J$-minimal move). Graded-rung cost extends the binary birth ledger to multi-valued phi-rung profiles: any unit-step phi-rung field pays $J(\varphi)$ per forced distinction, with the north star to carry each region at the coarsest rung recognition allows.

Integer rung gaps are too rigid once means are taken. Pair-resolve of integer levels can create half-rungs, so the invariant must be stated over $\mathbb{R}$: every listed edge has level gap at most one. That is the real-valued Phase-56 unit-step condition this module isolates.

The local theoretical setting is cosmology-side support for the forward dynamics: keep the graded field inside the unit-step regime so the graded cost law and equilibrium descent remain applicable after each mean move.

proof idea

The module is a small predicate-and-preservation package, not a single deep theorem. It defines the real unit-step predicate on an edge list and an edge-touching relation relative to a resolved pair. The main lemma is local: if the pre-resolve field is unit-step on every edge that touches the pair, then after both endpoints move to their mean the field is still unit-step on those edges (gap arithmetic under averaging).

Concrete witnesses $f_0,f_1,f_2$ and a three-edge chain supply explicit level assignments and edge lists; separate lemmas check unit-step at each stage and that the full chain remains unit-step under successive resolves. No heavy machinery beyond real absolute-value estimates and the imported equilibrium/cost vocabulary.

why it matters in Recognition Science

Without a real-valued unit-step invariant, pair-resolve would exit the hypothesis class of the graded-rung cost ledger (Phase 55 lineage) as soon as means create half-rungs. This module closes that gap for Phase-56-style reasoning: mean moves preserve gap-at-most-one on touched edges, so the $J(\varphi)$-per-distinction cost law and recognition-equilibrium descent stay applicable on the live graded engine.

It sits between GradedRungCost (cost law for unit-step phi-rung fields) and RecognitionEquilibrium (forward dynamics by pair-resolve to the $J$-ground state). No downstream Lean consumers are wired yet in the graph; the intended landing is any cosmogenesis or equilibrium theorem that must quote unit-step preservation after resolve. Framework landmarks: supports the multi-rung reading of the recognition composition / $J$-cost story rather than a new forcing-chain step (T5–T8).

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)