Qft Casimir Roughness

The roughness correction

The Casimir effect is a physical force: two uncharged metal plates in a vacuum attract each other when they are very close. Quantum field theory predicts this force because the space between the plates restricts which virtual particles can exist there, and the resulting pressure difference pushes the plates together. The force is tiny but real, and it has been measured in laboratories since the late 1990s. For perfectly smooth, parallel plates, the pressure depends only on the plate separation and a known constant.

Real plates are never perfectly smooth. Their surfaces have roughness and corrugation, and those imperfections change the force. The simplest correction treats roughness as a small dimensionless amplitude, the height variation h divided by the separation a. To first order in that ratio, the correction vanishes; the first nonzero effect is quadratic, proportional to (h/a)². This is a standard perturbative picture in physics: small irregularities modify an ideal result, and the leading correction is the square of the small parameter.

In Recognition Science, the framework models this correction explicitly. A ledger, a discrete record of recognition events, underlies the physical description, and the Casimir pressure is one of its derived quantities. The module defines a structural roughness coefficient, set to 1, and a roughness-corrected pressure: the ideal pressure multiplied by (1 + (h/a)²). The key equation is printed here once in full:

P_rough(h, a) = P_ideal(a) × (1 + (h/a)²).

The module then proves two facts about this definition. First, if the roughness amplitude h is zero, the corrected pressure equals the ideal pressure exactly. Second, if the roughness coefficient itself is set to zero, the same recovery holds for any amplitude. Both are trivial algebraic identities, but they are proved in a machine-checked library of formal theorems, meaning the recovery property is certified by the logic itself, not by hand-waving. The library also packages both proofs into a single certificate structure, a named object that records the two recovery guarantees.

What this establishes in plain language is a consistency check. The framework's model of roughness does not invent a new force; it starts from the ideal Casimir pressure and adds the smallest possible correction that respects the symmetry of the problem. The correction vanishes when roughness vanishes, and it vanishes when the coupling is turned off. That is exactly what a sane correction should do. The module does not derive the value of the roughness coefficient from deeper principles; it chooses 1 as a definitional starting point, and the recovery theorems hold for that choice.

The consequence is that the framework's Casimir account passes its first roughness test. A reader can now see that the correction is not an ad hoc patch but a controlled expansion with a certified limit. The next step, which remains open, is to derive the coefficient from the ledger dynamics rather than choosing it.

/-- Structural roughness coefficient. -/
noncomputable def roughnessCoefficient : ℝ := 1

/-- Roughness-corrected pressure. -/
noncomputable def roughnessCorrectedPressure (h : ℝ) (a : PlateSeparation) : ℝ :=
  idealPressure a * (1 + roughnessCoefficient * (h / a.value) ^ 2)

/-- Zero roughness recovers the ideal pressure. -/
theorem roughness_zero_recovers_ideal (a : PlateSeparation) :
    roughnessCorrectedPressure 0 a = idealPressure a := by
  unfold roughnessCorrectedPressure
  ring

/-- Zero roughness coefficient recovers the ideal pressure. -/
theorem roughness_zero_coefficient (h : ℝ) (a : PlateSeparation)
    (hcoef : roughnessCoefficient = 0) :
    roughnessCorrectedPressure h a = idealPressure a := by
  unfold roughnessCorrectedPressure
  rw [hcoef]
  ring

/-- Roughness correction certificate. -/
structure RoughnessCert where
  zero_roughness :
    ∀ a : PlateSeparation, roughnessCorrectedPressure 0 a = idealPressure a
  zero_coefficient :
    ∀ (h : ℝ) (a : PlateSeparation), roughnessCoefficient = 0 →
      roughnessCorrectedPressure h a = idealPressure a

/-- Certificate instance. -/
def roughnessCert : RoughnessCert where
  zero_roughness := roughness_zero_recovers_ideal
  zero_coefficient := roughness_zero_coefficient

What this page does not claim

The roughness coefficient 1 is not derived from deeper principles; it is a definitional choice. The module does not prove that the quadratic correction matches any specific experimental measurement. The recovery theorems are algebraic identities about the definition, not physical derivations of the Casimir effect itself.

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/CasimirRoughness.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: