Qft Casimir Torque

The anisotropic torque law

The Casimir effect is the force that empty space exerts between two uncharged, parallel plates. Quantum field theory (QFT) says the vacuum is not truly empty; it is full of fleeting particle-antiparticle pairs, and only certain wavelengths of these virtual particles can fit between the plates. The restricted set of allowed wavelengths creates a pressure that pushes the plates together. When the plates have an anisotropic surface, meaning their properties differ along different directions, the allowed wavelengths also depend on the angle between the plates' orientations. That angular dependence produces a torque, a twisting force that tries to rotate one plate relative to the other.

The standard structural law for this torque is sinusoidal in the relative angle. If θ is the angle between the plates' preferred directions, the torque is proportional to sin(2θ). The factor of 2 matters: it means the torque vanishes not only when the plates are aligned (θ = 0), but also when they are perpendicular (θ = π/2). The maximum twist occurs at θ = π/4, halfway between those two extrema. This is the classical behavior that experiments and theory have established for anisotropic Casimir systems.

In Recognition Science, the framework models physical structure as a ledger, a discrete record of recognition events, and derives constants and laws from the cost of maintaining that record. The Casimir torque module formalizes the standard sinusoidal law inside this framework. It defines the torque as a product of three factors: a coefficient β, the ideal energy density of the vacuum between the plates, and the sine of twice the angle. The module then proves three properties of this definition in its machine-checked library of formal theorems: the torque is zero at alignment, zero at orthogonal alignment, and reaches its full amplitude at a quarter turn.

These three results are not new physics; they are the basic sanity checks any acceptable torque law must satisfy. What the module adds is certainty. The proofs are checked by a computer, so there is no hidden assumption or unverified step in these three statements. The library also packages them into a single certificate structure, a formal object that bundles the three facts together. This certificate exists so that later modules can rely on the torque law without re-proving its simplest consequences. The practical upshot: within the framework, the anisotropic Casimir torque is a settled, machine-verified piece of the QFT structure, ready to be used as a building block for larger derivations.

/-- Aligned anisotropic plates have zero torque. -/
theorem torque_zero_at_aligned (beta : ℝ) (a : PlateSeparation) :
    casimirTorque beta a 0 = 0 := by
  unfold casimirTorque
  simp

/-- Orthogonal alignment also has zero torque in the `sin(2θ)` structural law. -/
theorem torque_zero_at_orthogonal (beta : ℝ) (a : PlateSeparation) :
    casimirTorque beta a (Real.pi / 2) = 0 := by
  unfold casimirTorque
  rw [show 2 * (Real.pi / 2) = Real.pi by ring]
  simp

/-- Quarter-turn alignment evaluates to the full anisotropic amplitude. -/
theorem torque_at_quarter_turn (beta : ℝ) (a : PlateSeparation) :
    casimirTorque beta a (Real.pi / 4) = beta * idealEnergyDensity a := by
  unfold casimirTorque
  rw [show 2 * (Real.pi / 4) = Real.pi / 2 by ring]
  rw [Real.sin_pi_div_two]
  ring

What this page does not claim

This module does not derive the coefficient β from first principles. It does not prove that the sinusoidal law follows from the framework's cost function. It does not make any new experimental prediction beyond the standard QFT result.

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/QFT/CasimirTorque.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: