Cosmology Recognition Unit Step Preservation Chain3 Levels

A three-step counterexample

In the Recognition Science framework, a ledger (a discrete record of events) assigns levels to sites, and an edge between two sites is allowed only if their levels differ by at most one. This is the unit-step invariant: adjacent rungs of the ladder stay close. The declaration chain3Levels defines the simplest nontrivial case, a chain of three sites with levels 0, 1, and 2. Before any update, the gaps are 1 and 1, so the invariant holds.

The framework then asks what happens when two neighboring sites resolve their difference by moving to their average, a mean-move update. The answer is surprising and precise: the invariant does not survive. Resolving the first edge of the 0-1-2 chain sends the levels to 1/2, 1/2, and 2. The second edge now has a gap of 3/2, which exceeds the allowed 1. The three-site chain is a proved counterexample, not a numerical accident.

The correct preservation statement is local, not global. A mean-move update preserves the unit-step invariant exactly when every edge touching the two resolved sites remains within one rung after the move. Edges that do not touch the resolved pair are unchanged and carry their old invariant automatically. This local criterion is what a runtime engine must audit before applying the cost law from earlier phases.

The upshot is a lesson in honesty: a tempting global lemma, that mean-move dynamics always preserves unit-step, is false. The framework's library proves the counterexample as a theorem and keeps the true local version alongside it. This is what the declaration chain3Levels establishes: not a sweeping guarantee, but a precise boundary on when a ledger can trust its own updates.

/-- The chain `0,1,2` is unit-step before any resolution. -/
theorem chain3_unitStep : UnitStepReal chain3Levels chain3Edges := by
  intro e he
  simp [chain3Edges] at he
  rcases he with rfl | he
  · norm_num
  · rcases he with rfl
    norm_num

/-- After resolving the first edge `(0,1)`, the second edge `(1,2)` has gap `3/2`. -/
lemma chain3_resolved_second_gap :
    |pairResolve chain3Levels f0 f1 f1 - pairResolve chain3Levels f0 f1 f2| = (3 / 2 : ℝ) := by
  have hf2_ne_f0 : f2 ≠ f0 := by decide
  have hf2_ne_f1 : f2 ≠ f1 := by decide
  rw [pairResolve_at_j, pairResolve_other chain3Levels hf2_ne_f0 hf2_ne_f1]
  norm_num

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

This does not claim that the unit-step invariant is preserved globally by any mean-move resolution. This does not claim that the three-site chain represents a physically realized cosmology; it is a formal counterexample. This does not claim that the local preservation criterion is always satisfied in practice; it is a condition to be audited.

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: