Foundation Measurement Mechanism

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

/-- **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 (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 (J-Cost Gives Born Weighting)**:
    Among all configurations compatible with the observer's partial view,
    the variational successor has the MAXIMUM J-cost weight (minimum defect).
    Other compatible configurations have lower weight (higher defect).

    The probability of an outcome is proportional to the total J-cost weight
    of all full states producing that outcome. Since the variational dynamics
    selects the minimum-defect state, the most probable outcome is the one
    that the actual dynamics produces. Near-optimal configurations contribute
    sub-leading probability, giving a distribution peaked at the actual outcome.

    For the specific form of J (quadratic near the minimum in log-coordinates:
    J(exp(t)) = cosh(t) - 1 ≈ t²/2), the resulting weight is Gaussian in
    log-ratio, which gives |ψ|²-like statistics under appropriate identification. -/
theorem jcost_born_structure {N : ℕ}
    (c : Configuration N) (next : Configuration N)
    (h : IsVariationalSuccessor c next) :
    ∀ c' ∈ Feasible c, jcost_weight c' ≤ jcost_weight next := by
  intro c' hc'
  unfold jcost_weight
  apply Real.exp_le_exp_of_le
  linarith [h.2 c' hc']