Encyclopedia Foundation Foundation Measurement Mechanism Correlation Is Permanent

ARTICLE 4 claims 4 theorems

Foundation Measurement Mechanism Correlation Is Permanent

When a measurement happens in this framework, the link it creates between observer and system never fades; the theorem says why, and what it leaves untouched.

Verify this page

The permanence of correlation

In the Recognition Science framework, a measurement is not a passive observation. It is an event that changes the state of the ledger, the framework's discrete record of all entries that exist. The theorem correlation_is_permanent states that once a measurement couples an observer subsystem to a system, the total defect of the combined configuration never increases at any later time step. The defect is a measure of how far a configuration is from the framework's ideal, lowest-cost state; a lower defect means a more ordered, more correlated configuration. The theorem proves that the act of measurement can only lock in or increase this order, never undo it.

The proof is a direct consequence of the framework's variational dynamics. Each step of a trajectory is chosen to minimize total defect among all feasible successor states. The theorem measurement_creates_correlation shows that after a coupling step, any alternative configuration that matches the observer's new entries but differs elsewhere must have at least as much defect. The permanence theorem then extends this from a single step to the entire future: for any time after the measurement, the defect is bounded above by its value at the measurement time. The framework's library, a machine-checked collection of formal theorems, verifies this chain of reasoning.

This permanence underpins the framework's account of apparent randomness. The theorem deterministic_but_unpredictable proves two facts together: the outcome of a measurement is a deterministic function of the full ledger state, and yet an observer who sees only a partial view cannot distinguish between full states that differ elsewhere. The permanence of correlation is what makes this distinction durable. Once a measurement creates a correlation, the observer's partial view remains tied to a specific full state forever, even though the observer cannot see the whole. The framework models this as the origin of apparent randomness, not as a failure of determinism.

The theorem does not claim that correlations are unbreakable in every physical sense. It proves that total defect never increases, but it does not prove that a later event cannot create a new correlation that masks an old one from an observer's view. It also does not claim that the observer can ever access the full state; the theorem subsystem_cannot_know_whole explicitly proves the opposite. The permanence is about the ledger's internal order, not about what any observer can know.

THEOREM correlation_is_permanent · IndisputableMonolith/Foundation/MeasurementMechanism.lean
correlation_is_permanent · IndisputableMonolith/Foundation/MeasurementMechanism.lean:280 
/-- **THEOREM (Correlation Is Permanent)**:
    Once created by a measurement (variational step), the correlation
    between observer and system entries cannot be undone by any future
    variational step — because defect is monotone decreasing.

    If the correlated state has defect d, any future state has defect ≤ d.
    Returning to an uncorrelated state with defect > d would violate
    defect monotonicity.

    This is decoherence: the measurement record is permanent. -/
theorem correlation_is_permanent {N : ℕ}
    (traj : Trajectory N)
    (h : IsVariationalTrajectory traj)
    (t_measure : ℕ) :
    ∀ t_future, t_measure ≤ t_future →
      total_defect (traj t_future) ≤ total_defect (traj t_measure) := by
  intro t_future ht
  rcases Nat.exists_eq_add_of_le ht with ⟨d, rfl⟩
  induction d with
  | zero =>
      simp
  | succ d ih =>
      calc
        total_defect (traj (t_measure + d.succ))
            = total_defect (traj ((t_measure + d) + 1)) := by simp [Nat.add_assoc]
        _ ≤ total_defect (traj (t_measure + d)) := trajectory_defect_monotone traj h (t_measure + d)
        _ ≤ total_defect (traj t_measure) := by
              simpa [Nat.add_assoc] using ih
THEOREM measurement_creates_correlation · IndisputableMonolith/Foundation/MeasurementMechanism.lean
measurement_creates_correlation · IndisputableMonolith/Foundation/MeasurementMechanism.lean:263 
/-- **THEOREM (Measurement Creates Correlation)**:
    After a variational step, the observer entries and system entries
    are generally correlated: changing a system entry while keeping the
    observer entries fixed violates the conservation constraint.

    This means the post-measurement state ENCODES information about the
    system in the observer's entries. This encoding IS the measurement. -/
theorem measurement_creates_correlation {N : ℕ} (hN : 2 ≤ N)
    (S : Subsystem N) (c : Configuration N)
    (next : Configuration N) (h : IsVariationalSuccessor c next) :
    ∀ (alt : Configuration N),
      (∀ i ∈ S.obs_indices, alt.entries i = next.entries i) →
      alt ∈ Feasible c →
      total_defect next ≤ total_defect alt := by
  intro alt _halt_obs halt_feas
  exact h.2 alt halt_feas
THEOREM deterministic_but_unpredictable · IndisputableMonolith/Foundation/MeasurementMechanism.lean
deterministic_but_unpredictable · IndisputableMonolith/Foundation/MeasurementMechanism.lean:352 
/-- **THEOREM (Deterministic But Unpredictable)**:
    The measurement outcome is:
    1. DETERMINED by the full state (outcome_is_determined)
    2. NOT DETERMINED by the observer's partial view (subsystem_cannot_know_whole)

    The apparent randomness is not ontological — it is epistemic.
    The universe is deterministic, but the observer is a part, not the whole.

    This resolves the measurement problem without:
    - Copenhagen collapse (no collapse — the full state evolves deterministically)
    - Many worlds (no branching — there is one trajectory)
    - Hidden variables (the "hidden" state IS the system entries) -/
theorem deterministic_but_unpredictable {N : ℕ} (S : Subsystem N)
    (space : OutcomeSpace) :
    -- 1. The outcome is a deterministic function of the full state
    (∀ c : Configuration N, ∃! k, outcome S space c = k) ∧
    -- 2. Observationally equivalent states exist with different entries
    (∃ c₁ c₂ : Configuration N,
      ObservationallyEquivalent S c₁ c₂ ∧ c₁.entries ≠ c₂.entries) :=
  ⟨fun c => outcome_is_determined S space c,
   subsystem_cannot_know_whole S⟩
THEOREM subsystem_cannot_know_whole · IndisputableMonolith/Foundation/MeasurementMechanism.lean
subsystem_cannot_know_whole · IndisputableMonolith/Foundation/MeasurementMechanism.lean:311 
/-- **THEOREM (Subsystem Information Is Insufficient)**:
    An observer that knows only its own K entries (out of N total) cannot
    determine the full N-entry state. The number of full states compatible
    with any given partial view is uncountably infinite (for K < N).

    This is not a practical limitation — it is a structural impossibility.
    The observer is a PART of the ledger and cannot access the WHOLE. -/
theorem subsystem_cannot_know_whole {N : ℕ} (S : Subsystem N) :
    ∃ (c₁ c₂ : Configuration N),
      ObservationallyEquivalent S c₁ c₂ ∧ c₁.entries ≠ c₂.entries := by
  have hK_lt := S.hK_lt
  have hcompl : (S.sys_indices).Nonempty := by
    rw [Finset.nonempty_iff_ne_empty]
    intro h_empty
    have : S.sys_indices.card = 0 := by rw [h_empty]; exact Finset.card_empty
    rw [S.sys_card] at this
    omega
  obtain ⟨j, hj⟩ := hcompl
  have hj_not_obs : j ∉ S.obs_indices := by
    intro h_in
    have := Finset.mem_sdiff.mp hj
    exact this.2 h_in
  let c₁ : Configuration N := {
    entries := fun _ => 1
    entries_pos := fun _ => by norm_num
  }
  let c₂ : Configuration N := {
    entries := fun i => if i = j then 2 else 1
    entries_pos := fun i => by
      by_cases hij : i = j <;> simp [hij] <;> norm_num
  }
  use c₁, c₂
  constructor
  · intro i hi
    simp only [c₁, c₂]
    have : i ≠ j := fun h_eq => hj_not_obs (h_eq ▸ hi)
    simp [this]
  · intro h_eq
    have : c₁.entries j = c₂.entries j := congrFun h_eq j
    simp [c₁, c₂] at this

What this page does not claim

The theorem does not claim that correlations are unbreakable in every physical sense. It does not claim that a later event cannot create a new correlation that masks an old one from an observer's view. It does not claim that the observer can ever access the full state.

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/Foundation/MeasurementMechanism.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND