Cosmology Recognition Unit Step Preservation Unit Step Real

Unit-step fields

A unit-step field is a way of assigning real numbers, called levels, to the points of a network, with one rule: along every listed connection, the two levels may differ by at most one. Think of a row of shelves where neighboring shelves can hold items of similar height, but no two connected shelves can jump by more than one unit. The declaration UnitStepReal in the framework's machine-checked library of formal theorems states this condition precisely: for every edge in a finite list, the absolute difference between the two endpoint levels is at most one.

The interesting question is what happens when the network updates itself. The framework models a move called pairResolve, where two connected points are averaged toward each other, a kind of local reconciliation. The library proves a local preservation theorem: if every edge touching the resolved pair still satisfies the unit-step condition after the move, then the whole network remains unit-step. Edges that do not touch the resolved pair are unchanged, so they keep their old property automatically. This is the exact condition a runtime engine must check before applying the cost law to an actively updated field.

The framework also proves that a global preservation claim would be false. Consider a three-site chain with levels 0, 1, 2. It satisfies the unit-step condition, since each gap is exactly 1. Resolving the first edge sends the levels to 1/2, 1/2, 2, and now the second edge has a gap of 3/2, which violates the rule. This counterexample is a theorem, not a numerical observation: the framework's library shows that the naive statement "mean-move preserves UnitStep" is false, and that the local condition is necessary rather than cosmetic.

The upshot is precise. The live engine may use the Phase-56 cost law only after auditing or proving the local unit-step condition for the update being applied. A blind global lemma would be wrong. What the declaration establishes is a sharp boundary: preservation holds exactly under the local post-move edge condition, and fails without it. This is the honest theorem layer, with no gaps and no new axioms beyond the standard classical ones.

/-- A real-valued version of the Phase-56 unit-step invariant: every listed edge has
level gap at most one. This is the right formulation for `pairResolve`, whose mean move
can create half-rungs even when the input levels are integer rungs. -/
def UnitStepReal {n : ℕ} (x : Fin n → ℝ) (E : List (Fin n × Fin n)) : Prop :=
  ∀ e ∈ E, |x e.1 - x e.2| ≤ 1

/-- **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 declaration does not claim that mean-move dynamics preserves unit-step globally; it proves the opposite. The declaration does not establish any physical law about cosmology or space-time. The declaration does not claim that the local condition is easy to verify in practice.

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: