StatMech.v

(** * Statistical Mechanics and Thermodynamics of Computation

    This module formalizes the statistical mechanical foundations of
    Certified Null Operations, proving rigorous connections to
    Landauer's Principle and thermodynamic reversibility.

    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
    License: MPL-2.0
*)

Require Import Coq.Reals.Reals.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Lists.List.
Require Import Coq.micromega.Psatz.
Require Import CNO.CNO.
(* Shared physics constants — kB, temperature, kB_positive,
   temperature_positive. See proofs/coq/common/PhysicsConstants.v
   (consolidated by Follow-up 1 of docs/proof-debt-triage.md). *)
Require Import CNO.PhysicsConstants.
(* Shared statmech basis — StateDistribution, prob_nonneg, prob_normalized,
   state_dec, point_dist, shannon_entropy, shannon_entropy_nonneg,
   shannon_entropy_point_zero. See proofs/coq/common/StatMechBasis.v
   (consolidated by Follow-up 3 of docs/proof-debt-triage.md). *)
Require Import CNO.StatMechBasis.
Import ListNotations.

Open Scope R_scope.

(** ** Physical Constants

    [kB], [temperature], [kB_positive], and [temperature_positive] are
    imported from [CNO.PhysicsConstants] (consolidated by Follow-up 1).
    In SI units: [kB ≈ 1.380649×10⁻²³ J/K]; room temperature ≈ 300 K. *)

(** ** Probability Distributions, Entropy

    [StateDistribution], [prob_nonneg], [prob_normalized], [state_dec],
    [point_dist], [shannon_entropy], [shannon_entropy_nonneg], and
    [shannon_entropy_point_zero] are imported from [CNO.StatMechBasis]
    (consolidated by Follow-up 3 of [docs/proof-debt-triage.md]). *)

(** Axiom: Entropy is maximized for uniform distribution *)
(* NOT-YET-DISCHARGED (class A) + SOUNDNESS WARNING: the statement is
   mathematically INCORRECT as written and cannot be proved without changing its
   meaning. It reads: if [P] is constant on [states], then [H(P) <= H(P')] for
   *every* other distribution [P']. That asserts a uniform distribution has the
   MINIMUM entropy and lower-bounds all others — the reverse of the Gibbs
   inequality (uniform MAXIMIZES entropy). Worse, taking [states := []] makes the
   constancy hypothesis vacuously true for any [P], yielding [H(P) <= H(P')] for
   all [P, P'] (all entropies equal). The correct statement is
   [H(P') <= H(P) = log₂|support|] for [P'] supported on the same finite set.
   This axiom is UNUSED downstream. BLOCKER: cannot discharge the current
   (false) statement; recommend replacing it with the correct Gibbs bound, whose
   proof then needs a concrete [shannon_entropy] and finite-support machinery. *)
(* AXIOM: [CLASS-A] maximum entropy bound for uniform distribution pending finite support machinery. *)
Axiom shannon_entropy_maximum :
  forall (P : StateDistribution) (states : list ProgramState),
    (forall s1 s2, In s1 states -> In s2 states -> P s1 = P s2) ->
    forall P', shannon_entropy P <= shannon_entropy P'.

(** Change in entropy *)
Definition entropy_change (P_initial P_final : StateDistribution) : R :=
  shannon_entropy P_final - shannon_entropy P_initial.

(** ** Thermodynamic Entropy *)

(** Boltzmann entropy: S = kB ln(2) H (relating information to thermodynamics)

    The factor ln(2) converts from bits (log₂) to nats (ln)
*)
Definition boltzmann_entropy (P : StateDistribution) : R :=
  kB * ln 2 * shannon_entropy P.

Theorem boltzmann_entropy_nonneg :
  forall P : StateDistribution,
    boltzmann_entropy P >= 0.
Proof.
  intros P.
  unfold boltzmann_entropy.
  pose proof kB_positive as HkB.
  pose proof (shannon_entropy_nonneg P) as Hentropy.
  unfold Rge in Hentropy.
  pose proof ln_lt_2 as Hln_half.
  assert (Hln : ln 2 > 0) by lra.
  unfold Rge.
  destruct Hentropy as [Hentropy_pos | Hentropy_zero].
  - left.
    replace (kB * ln 2 * shannon_entropy P)%R
      with ((kB * ln 2) * shannon_entropy P)%R by ring.
    apply Rmult_lt_0_compat.
    + apply Rmult_lt_0_compat; assumption.
    + exact Hentropy_pos.
  - right. rewrite Hentropy_zero. ring.
Qed.

(** ** Landauer's Principle *)

(** Landauer's Principle (1961): Erasing one bit of information
    dissipates at least kT ln(2) joules of energy.

    More generally: E_dissipated >= kT ΔS
    where ΔS is the change in thermodynamic entropy.

    This is a PHYSICAL LAW, not a mathematical theorem.
    We axiomatize it from experimental physics.
*)

(** Energy dissipated by a computational process (Joules) *)
(* METAL-BOUNDARY (kept): [energy_dissipated_phys] is a physical observable
   (heat released to the environment, in Joules) attached to a process taking one
   distribution to another. It is an opaque [Parameter] representing a measured
   physical quantity, not a derivable mathematical function. *)
(* AXIOM: [METAL-BOUNDARY] physical observable of heat released by computational transition (Joules). *)
Parameter energy_dissipated_phys : StateDistribution -> StateDistribution -> R.

(* METAL-BOUNDARY AXIOM (kept): Landauer's principle (1961) is an EMPIRICAL
   physical law of thermodynamics — erasing information dissipates at least
   [kB·T·ln2·(-ΔS)] of energy. It is not a mathematical theorem; it is a lower
   bound imposed by the second law on physical realizations of computation.
   Correctly kept as a physical postulate (the module comment above already
   states "This is a PHYSICAL LAW, not a mathematical theorem"). *)
(* AXIOM: [METAL-BOUNDARY] Landauer 1961 empirical thermodynamic lower bound on information erasure. *)
Axiom landauer_principle :
  forall (P_initial P_final : StateDistribution),
    let ΔS := shannon_entropy P_final - shannon_entropy P_initial in
    ΔS < 0 ->  (* Information was erased *)
    energy_dissipated_phys P_initial P_final >=
      kB * temperature * ln 2 * (-ΔS).

(** Landauer minimum (energy per bit erased) *)
Definition landauer_limit : R := kB * temperature * ln 2.

Theorem landauer_limit_positive : landauer_limit > 0.
Proof.
  unfold landauer_limit.
  apply Rmult_lt_0_compat.
  - apply Rmult_lt_0_compat.
    + apply kB_positive.
    + apply temperature_positive.
  - pose proof ln_lt_2 as Hln_half. lra.
Qed.

(** At room temperature (300K): E_min ≈ 2.85 × 10⁻²¹ J per bit *)

(** ** CNO Thermodynamics *)

(** Key insight: CNOs preserve state deterministically,
    so they preserve entropy. *)

(** Distribution after program execution

    Formally, for a deterministic program p:
    P_final(s_final) = Σ_{s_initial} P_initial(s_initial) × δ(f_p(s_initial), s_final)

    where:
    - f_p is the state transformation function induced by p
    - δ is the Kronecker delta: δ(x,y) = 1 if x=y, 0 otherwise

    For CNOs where f_p = id (identity), this simplifies to:
    P_final(s) = Σ_{s'} P_initial(s') × δ(s', s) = P_initial(s)

    The implementation directly uses this simplification for CNOs.
*)
Definition post_execution_dist
  (p : Program) (P_initial : StateDistribution) : StateDistribution :=
  fun s_final =>
    (* For a CNO, the transformation function is identity.
       Therefore: P_final(s) = P_initial(s)

       General case would require:
       - A function eval_to_state : Program -> ProgramState -> ProgramState
       - Summation over all states (requires measure theory for infinite states)
       - Kronecker delta comparison

       The identity case is exact and requires no approximation.
    *)
    P_initial s_final.

(** Justification for the identity simplification:

    For any CNO p:
    1. By definition of CNO: ∀s, eval p s s  (state preservation)
    2. Therefore f_p(s) = s for all s  (identity function)
    3. Substituting into the distribution formula:
       P_final(s) = Σ_{s'} P_initial(s') × δ(id(s'), s)
                  = Σ_{s'} P_initial(s') × δ(s', s)
                  = P_initial(s)  (by definition of δ)

    This is not a placeholder - it is the mathematically correct result
    for the specific case of CNOs.
*)

(** CNOs preserve entropy *)
Theorem cno_preserves_shannon_entropy :
  forall (p : Program) (P : StateDistribution),
    is_CNO p ->
    shannon_entropy (post_execution_dist p P) = shannon_entropy P.
Proof.
  intros p P H_cno.
  unfold post_execution_dist.
  (* For a CNO, eval p s = s for all s *)
  (* Therefore the distribution is unchanged *)
  reflexivity.
Qed.

(** Corollary: CNOs have zero entropy change *)
Theorem cno_zero_entropy_change :
  forall (p : Program) (P : StateDistribution),
    is_CNO p ->
    entropy_change P (post_execution_dist p P) = 0.
Proof.
  intros p P H_cno.
  unfold entropy_change.
  rewrite cno_preserves_shannon_entropy; auto.
  ring.
Qed.

(** Physical axiom: Reversible processes (ΔS = 0) dissipate no energy *)
(** This is a consequence of Landauer's Principle and thermodynamic reversibility *)
(* METAL-BOUNDARY AXIOM (kept). CLASSIFICATION CORRECTION: the triage docs mark
   this "DISCHARGE / derivable from landauer_principle + reversibility", but it is
   NOT derivable from the present machinery. [landauer_principle] only gives a
   *lower* bound on [energy_dissipated_phys] when ΔS < 0; for ΔS = 0 it says
   nothing, and there is no upper-bound axiom on the opaque
   [energy_dissipated_phys], so [= 0] cannot be proved. The statement
   "zero entropy change ⇒ zero dissipation" is itself an additional physical
   postulate (thermodynamic reversibility), so it is honestly kept as a
   metal-boundary axiom rather than fake-derived. *)
(* AXIOM: [METAL-BOUNDARY] thermodynamic reversibility postulate (zero entropy change implies zero dissipation). *)
Axiom reversible_zero_dissipation :
  forall P_initial P_final : StateDistribution,
    shannon_entropy P_initial = shannon_entropy P_final ->
    energy_dissipated_phys P_initial P_final = 0.

(** Main Theorem: CNOs dissipate zero energy (by Landauer's Principle) *)
Theorem cno_zero_energy_dissipation :
  forall (p : Program) (P : StateDistribution),
    is_CNO p ->
    energy_dissipated_phys P (post_execution_dist p P) = 0.
Proof.
  intros p P H_cno.
  (* Apply the axiom that reversible processes (ΔS = 0) dissipate no energy *)
  apply reversible_zero_dissipation.
  (* CNOs preserve entropy *)
  symmetry.
  apply cno_preserves_shannon_entropy.
  exact H_cno.
Qed.

(** ** Bennett's Reversible Computing *)

(** Bennett (1973): Computation can be made thermodynamically reversible
    by never erasing information, only permuting it. *)

(** A program is logically reversible up to observational equivalence:
    there exists an inverse program that, run on the post-execution state,
    recovers a state observationally equal ([=st=]) to the input.

    Stating reversibility up to [=st=] (rather than strict [=]) is forced
    by the rescue branch's PC-excluding [state_eq]: [eval p s s'] uniquely
    determines [s'] (cf. [eval_deterministic_strong]) including its PC,
    so re-running [p] on a different start state cannot in general produce
    a PC-identical result. Observational reversibility is what the
    thermodynamic argument actually needs (memory + registers + I/O are
    the bits of physical record; the PC is bookkeeping). See ADR-008
    (2026-05-20). *)
Definition logically_reversible (p : Program) : Prop :=
  exists p_inv : Program,
    forall s s',
      eval p s s' ->
      exists s'', eval p_inv s' s'' /\ s'' =st= s.

(** Logical reversibility implies thermodynamic reversibility *)

(** NOTE ON PROOF STRENGTH:
    This proof is trivially true under the current definition of
    post_execution_dist, which is specialized for CNOs (identity on
    distributions). The logically_reversible hypothesis is not used.

    For a fully general proof that works with arbitrary reversible programs,
    one would need:
    1. A general post_execution_dist_general using eval_to_state functions
    2. A proof that bijective state transformations preserve Shannon entropy
    3. Measure theory for infinite state spaces

    The conceptual argument (Bennett 1973):
    - Logically reversible programs induce bijections on state space
    - Bijections preserve the measure of any measurable set
    - Therefore bijections preserve Shannon entropy
    - Therefore logically reversible programs are thermodynamically reversible

    This is recorded as a TODO for the v1.0 generalization milestone.
*)
Theorem bennett_logical_implies_thermodynamic :
  forall (p : Program) (P : StateDistribution),
    logically_reversible p ->
    shannon_entropy P = shannon_entropy (post_execution_dist p P).
Proof.
  intros p P H_rev.
  (* post_execution_dist is defined as identity on distributions
     (specialized for CNOs where f_p = id), so this holds by
     definitional equality via eta-conversion. *)
  unfold post_execution_dist.
  reflexivity.
Qed.

(** CNOs are trivially logically reversible (identity is its own inverse) *)
Theorem cno_logically_reversible :
  forall p : Program,
    is_CNO p ->
    logically_reversible p.
Proof.
  intros p H_cno.
  unfold logically_reversible.
  exists p.  (* CNO is its own inverse *)
  intros s s' H_eval.

  (* Key insight: For a CNO, eval p s s' implies s =st= s'
     So "reversing" just means running p again on s', which maps back to s.
     Since s =st= s', running p on s' gives a result =st= to s'. *)

  (* Step 1: CNO property gives us s =st= s' *)
  assert (s =st= s') as H_state_eq.
  { apply cno_preserves_state with (p := p) (s := s) (s' := s').
    - assumption.
    - assumption. }

  (* Step 2: By termination, eval p s' s'' for some s'' *)
  destruct (cno_terminates p H_cno s') as [s'' H_eval'].

  (* Step 3: By CNO identity property, s' =st= s'' *)
  assert (s' =st= s'') as H_s'_eq_s''.
  { apply cno_preserves_state with (p := p) (s := s') (s' := s'').
    - assumption.
    - assumption. }

  (* Step 4: By transitivity, s'' =st= s *)
  assert (s'' =st= s) as H_s''_eq_s.
  { apply state_eq_trans with (s2 := s').
    - apply state_eq_sym. exact H_s'_eq_s''.
    - apply state_eq_sym. exact H_state_eq. }

  (* Step 5: We have eval p s' s'' and s'' =st= s.
     The (now weakened) definition of [logically_reversible] only requires
     a witness end-state observationally equal to s — H_eval' + H_s''_eq_s
     supply it directly. The previous proof used the unsound
     [eval_respects_state_eq_right] axiom; that axiom has been removed
     (see CNO.v / ADR-008). *)
  exists s''. split; [ exact H_eval' | exact H_s''_eq_s ].
Qed.

(** ** Physical Implications *)

(** Thermodynamic efficiency: Ratio of minimum energy to actual energy *)
Definition thermodynamic_efficiency
  (P_i P_f : StateDistribution) : R :=
  let ΔS := shannon_entropy P_f - shannon_entropy P_i in
  if Rlt_dec ΔS 0 then
    (kB * temperature * ln 2 * (-ΔS)) /
    energy_dissipated_phys P_i P_f
  else
    1.  (* No erasure, maximum efficiency *)

(** CNOs achieve maximum thermodynamic efficiency *)
Theorem cno_maximum_efficiency :
  forall (p : Program) (P : StateDistribution),
    is_CNO p ->
    thermodynamic_efficiency P (post_execution_dist p P) = 1.
Proof.
  intros p P H_cno.
  unfold thermodynamic_efficiency.
  rewrite cno_preserves_shannon_entropy; auto.
  simpl.
  (* ΔS = 0, so we're in the else branch *)
  destruct Rlt_dec; [lra | reflexivity].
Qed.

(** ** Connection to Original CNO Definition *)

(** Our original energy_dissipated was symbolic. Now we connect it
    to physical energy dissipation. *)

Theorem symbolic_energy_matches_physical :
  forall (p : Program) (s1 s2 : ProgramState),
    eval p s1 s2 ->
    is_CNO p ->
    CNO.energy_dissipated p s1 s2 = 0%nat <->
    energy_dissipated_phys (point_dist s1) (post_execution_dist p (point_dist s1)) = 0.
Proof.
  intros p s1 s2 H_eval H_cno.
  split; intros H.
  - (* -> direction *)
    apply cno_zero_energy_dissipation.
    assumption.
  - (* <- direction *)
    unfold CNO.energy_dissipated.
    reflexivity.
Qed.

(** ** Summary *)

(** This module proves:

    1. CNOs preserve information-theoretic entropy (Shannon)
    2. CNOs preserve thermodynamic entropy (Boltzmann)
    3. By Landauer's Principle, CNOs dissipate zero energy
    4. CNOs achieve maximum thermodynamic efficiency
    5. CNOs are reversible in Bennett's sense

    The connection from abstract programs to physical thermodynamics
    is now rigorously formalized, not just asserted.
*)