Cosmology Recognition Unit Step Preservation Pair Resolve Unit Step Of Local

The local preservation theorem

In the Recognition Science framework, a ledger (a discrete record of events) assigns a real-valued level to each site in a finite network. The unit-step invariant, a real-valued version of the Phase-56 graded-rung cost law, requires that every edge in the network connects sites whose levels differ by at most 1. The question is whether the active mean-move dynamics, which resolves a pair of sites by replacing their levels with their average, preserves this invariant automatically. The tempting global claim is false.

The theorem pairResolve_unitStep_of_local establishes the precise condition under which preservation does hold. If every edge touching the resolved pair remains unit-step after the move, then the whole edge list remains unit-step. Edges disjoint from the resolved pair are unchanged by the move, so their old unit-step property carries over for free. The theorem is proved in the machine-checked library of formal theorems with no admitted axioms beyond the standard classical ones; it is a THEOREM, not a numerical observation.

The necessity of the local condition is demonstrated by a counterexample, also proved as a theorem. A three-site chain with levels 0, 1, 2 is unit-step before any resolution. Resolving the first edge sends the levels to 1/2, 1/2, 2, so the second edge has gap 3/2 and the invariant fails. This blocks the false global lemma "mean-move preserves UnitStep" and shows the local post-move edge condition is necessary rather than cosmetic.

The upshot for the runtime engine is direct: the Phase-56 cost law may be applied to an actively updated field only after auditing or proving the local unit-step condition for the update being applied. The theorem does not claim that the mean-move dynamics preserves the unit-step invariant globally, nor that the local condition is always satisfied in practice. It provides the exact criterion to check, and the counterexample shows why the check matters.

/-- **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 mean-move dynamics preserves the unit-step invariant globally for all edge lists. The local condition is always satisfied by the active recognition dynamics. The unit-step invariant is the only constraint governing recognition costs.

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: