Cosmology Recognition Unit Step Preservation Edge Touches

The local condition

In a discrete model where points carry levels and connections link them, a recognition event (a discrete record of a comparison) often updates the levels of two points at once. The question is whether such an update can break a simple rule: that every connection links points whose levels differ by at most one. The declaration EdgeTouches answers the first part of that question. It defines, for any two points being updated, which connections are affected: a connection touches the pair if either of its endpoints is one of the two points. This is a definition, not a theorem; it names the set of connections that could possibly change.

The theorem that follows is the useful part. It proves that if every connection touching the updated pair still satisfies the one-level gap rule after the update, then the whole collection of connections still satisfies the rule. Connections that do not touch the pair are unchanged by the update, so their old status carries over automatically. The proof is machine-checked in the framework's library of formal theorems, with no gaps and no extra assumptions beyond standard logic.

The declaration also establishes what is not true. A tempting global claim would be that any such update preserves the rule everywhere, with no further checking. That claim is false. The library proves a concrete counterexample: a chain of three points with levels 0, 1, and 2. Updating the first connection sends the levels to 1/2, 1/2, and 2, so the second connection now has a gap of 3/2, which violates the rule. The local condition is therefore necessary, not a formality.

In practice, this means an engine that updates levels must audit the connections touching each updated pair, or prove the local condition for its specific update rule, before relying on the one-level gap law. The declaration does not claim that the local condition always holds, nor that any particular update rule satisfies it. It only defines the set of connections to check and proves that checking them is sufficient.

/-- An edge touches the pair being resolved if either endpoint is one of the two
resolved vertices. -/
def EdgeTouches {n : ℕ} (i j : Fin n) (e : Fin n × Fin n) : Prop :=
  e.1 = i ∨ e.1 = j ∨ e.2 = i ∨ e.2 = j

/-- **Local preservation criterion.** A `pairResolve` move preserves the unit-step
invariant on the whole edge list if every edge touching the resolved pair remains
unit-step after the move. Disjoint edges are unchanged by `pairResolve_other`, so the
old unit-step invariant carries them automatically.

This is the exact condition the runtime must audit, or a later theorem must prove, before
applying the Phase-56 cost law to an actively updated field. -/
theorem pairResolve_unitStep_of_local {n : ℕ} (x : Fin n → ℝ) (E : List (Fin n × Fin n))
    (i j : Fin n) (hunit : UnitStepReal x E)
    (hlocal : ∀ e ∈ E, EdgeTouches i j e →
      |pairResolve x i j e.1 - pairResolve x i j e.2| ≤ 1) :
    UnitStepReal (pairResolve x i j) E := by
  intro e he
  by_cases ht : EdgeTouches i j e
  · exact hlocal e he ht
  · have h1i : e.1 ≠ i := by
      intro h; exact ht (Or.inl h)
    have h1j : e.1 ≠ j := by
      intro h; exact ht (Or.inr (Or.inl h))
    have h2i : e.2 ≠ i := by
      intro h; exact ht (Or.inr (Or.inr (Or.inl h)))
    have h2j : e.2 ≠ j := by
      intro h; exact ht (Or.inr (Or.inr (Or.inr h)))
    rw [pairResolve_other x h1i h1j, pairResolve_other x h2i h2j]
    exact hunit e he

/-- **Counterexample.** A unit-step field need not remain unit-step after a mean-move
resolution. The three-site chain `0 -- 1 -- 2` starts with gaps `1` and `1`; resolving
the first edge gives levels `1/2, 1/2, 2`, so the second edge has gap `3/2 > 1`.

This blocks the false global theorem "mean-move preserves UnitStep". The correct theorem
is the local criterion `pairResolve_unitStep_of_local` above. -/
theorem chain3_pairResolve_breaks_unitStep :
    ¬ UnitStepReal (pairResolve chain3Levels f0 f1) chain3Edges := by
  intro h
  have hedge : (f1, f2) ∈ chain3Edges := by
    simp [chain3Edges]
  have hstep := h (f1, f2) hedge
  rw [chain3_resolved_second_gap] at hstep
  norm_num at hstep

What this page does not claim

The local condition always holds for any update. Any particular update rule satisfies the condition. The one-level gap rule is preserved globally without checking.

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/RecognitionUnitStepPreservation.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: