OAI/Probability/InvariantIsing/Cavity/CavityPhysicalFrameOrbit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single reservoir rotation represents both the base interaction and its selected special axes, as needed for the fresh-frame law.

  1. lemma OAI.InvariantIsing.cavityReservoir_spectral_eq line 13
  2. def OAI.InvariantIsing.cavityCanonicalSpecial line 29
  3. lemma OAI.InvariantIsing.cavityCanonicalSpecial_mul line 32
  4. theorem OAI.InvariantIsing.cavityBaseReplacement_physical_joint_orbit line 38