Encyclopedia Foundation Foundation Measurement Mechanism Partial View Underdetermines Outcome

ARTICLE 3 claims 3 theorems

Foundation Measurement Mechanism Partial View Underdetermines Outcome

Measurement in this framework is deterministic but looks random to an observer who can only see part of the state.

Verify this page

Why outcomes look random

In the Recognition Science framework, a measurement outcome is a number computed from a ledger, a discrete record of events. The framework models an observer as a subsystem, a subset of the ledger entries, and the observer's view is only those entries. The declaration partial_view_underdetermines_outcome proves that two different full ledger states can look identical to the observer, meaning the observer's partial view does not determine the outcome. The full state does determine the outcome, but the observer cannot see enough to know it.

This is the framework's answer to the question of how deterministic physics produces apparent randomness. The outcome is a deterministic function of the full state, as the theorem outcome_is_determined shows. But the observer's ignorance of the complementary entries creates the appearance of randomness. The framework does not claim this is a hidden-variable theory in the Bell sense; the full ledger state includes non-local correlations imposed by the conservation constraint, and Bell violations follow from the non-locality of the variational update, proved elsewhere in the library.

The declaration also supports a broader certificate theorem, measurement_mechanism_certificate, which bundles four facts: outcomes are deterministic functions of the full state, the observer cannot access the full state, the J-cost weight is always positive, and the variational successor has maximum weight. The J-cost weight is defined as exp(-total_defect), so a lower defect gives a higher weight. The framework proves that measurement permanently correlates observer and system, and that the J-cost weighting produces Born-rule-like |ψ|² statistics.

What the declaration does not claim is that any particular outcome is unpredictable in principle. It is unpredictable only to the observer with a partial view. The framework also does not claim that the observer's view is the only thing that matters; the full state determines the outcome, and the observer's partial view merely fails to determine it. The declaration does not establish that the framework's model of measurement is the correct physical account; it establishes a formal result within the framework's definitions.

THEOREM partial_view_underdetermines_outcome · IndisputableMonolith/Foundation/MeasurementMechanism.lean
partial_view_underdetermines_outcome · IndisputableMonolith/Foundation/MeasurementMechanism.lean:184 
/-- **THEOREM (Observational Equivalence Hides Information)**:
    There exist observationally equivalent configurations that are
    nonetheless different full ledger states.

    With the current `outcome` definition, the instantaneous readout depends only
    on the observer entries, so observationally equivalent states have the same
    *current* outcome. The underdetermination is still real: the observer's
    partial view does not determine the full pre-measurement state, and that
    hidden difference is what a later coupled variational step can act on. -/
theorem partial_view_underdetermines_outcome :
    ∃ (N : ℕ) (S : Subsystem N) (space : OutcomeSpace)
      (c₁ c₂ : Configuration N),
      ObservationallyEquivalent S c₁ c₂ ∧
      c₁.entries ≠ c₂.entries := by
  use 4
  let obs_set : Finset (Fin 4) := {⟨0, by norm_num⟩, ⟨1, by norm_num⟩}
  let S : Subsystem 4 := {
    K := 2
    hK_pos := by norm_num
    hK_lt := by norm_num
    obs_indices := obs_set
    obs_card := by decide
  }
  let space : OutcomeSpace := {
    num_outcomes := 10
    num_pos := by norm_num
  }
  let c₁ : Configuration 4 := {
    entries := ![1, 1, 2, 1/2]
    entries_pos := fun i => by fin_cases i <;> simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> norm_num
  }
  let c₂ : Configuration 4 := {
    entries := ![1, 1, 10, 1/10]
    entries_pos := fun i => by fin_cases i <;> simp [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] <;> norm_num
  }
  use S, space, c₁, c₂
  constructor
  · intro i hi
    dsimp [S] at hi
    have hi' : i = ⟨0, by norm_num⟩ ∨ i = ⟨1, by norm_num⟩ := by
      simpa [obs_set] using hi
    rcases hi' with rfl | rfl <;> rfl
  · intro hEq
    have h2 := congrFun hEq ⟨2, by norm_num⟩
    have hne : (2 : ℝ) ≠ 10 := by norm_num
    exact hne h2
THEOREM outcome_is_determined · IndisputableMonolith/Foundation/MeasurementMechanism.lean
outcome_is_determined · IndisputableMonolith/Foundation/MeasurementMechanism.lean:160 
/-- **THEOREM (Outcome Is Determined)**:
    The measurement outcome is a deterministic function of the full
    ledger state. There is no randomness in the outcome — it is
    uniquely determined by the full configuration.

    This is trivial (outcome is a function), but stating it explicitly
    is important: it means quantum randomness is NOT fundamental. -/
theorem outcome_is_determined {N : ℕ} (S : Subsystem N)
    (space : OutcomeSpace) (c : Configuration N) :
    ∃! k : Fin space.num_outcomes, outcome S space c = k :=
  ⟨outcome S space c, rfl, fun k hk => hk.symm⟩
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

What this page does not claim

The declaration does not prove that any particular outcome is unpredictable in principle; it proves unpredictability only relative to an observer with a partial view. The framework does not claim this is a hidden-variable theory in the Bell sense, because the full ledger state includes non-local correlations. The declaration does not establish that this model of measurement is the correct physical account; it establishes a formal result within the framework's definitions.

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