Qft Casimir Numerical Bounds

The pressure interval

The Casimir effect is a real, measurable force: two uncharged metal plates in a vacuum attract each other because quantum fields between them have fewer allowed modes than outside. In 1948 Hendrik Casimir predicted the pressure between perfect conducting plates, and experiments have since confirmed it to high precision. The standard formula, for plates of area A separated by distance d, gives a pressure proportional to −ħc/d⁴, where the minus sign means attraction.

In the Recognition Science (RS) framework, the same physics emerges from a discrete ledger of recognition events, a record of what the framework counts as happening. The framework's constants are not free parameters: its unit system sets ħ = φ⁻⁵ and G = φ⁵/π, with c = 1, so all quantities become pure numbers. At unit plate separation, the ideal Casimir pressure magnitude becomes a specific real number, defined as the negative of the ideal pressure.

What the module proves is deliberately modest. It shows, with a machine-checked library of formal theorems, that this unit-separation pressure magnitude is positive and less than 1. The upper bound uses only three crude facts: π < 4, ħ < 1, and c = 1. No numerical fitting, no approximations beyond those inequalities, no hidden assumptions. The result is a certificate: a formal object that records the interval (0, 1) for the pressure magnitude at unit separation.

The practical use of this bound is falsification. The module defines a falsifier structure: if a future measurement at unit separation reports a magnitude outside (0, 1), that measurement contradicts the framework's prediction. The interval is wide, but it is exact and machine-checked. It turns the Casimir effect into a testable prediction with a named condition for failure.

In plain language: the framework says the Casimir pressure at unit separation has a magnitude between 0 and 1 in its natural units, and it proves that bound rigorously. The bound is not tight, but it is honest. It gives experimenters a concrete number to shoot at, and it shows that the framework's constants, though unusual, produce a finite and bounded prediction for a real physical effect.

/-- Unit-separation Casimir pressure magnitude is positive. -/
theorem unitPressureMagnitude_pos :
    0 < unitPressureMagnitude := by
  unfold unitPressureMagnitude
  exact neg_pos.mpr (idealPressure_negative unitSeparation)

/-- Conservative explicit upper bound at unit RS separation. -/
theorem unitPressureMagnitude_lt_one :
    unitPressureMagnitude < 1 := by
  unfold unitPressureMagnitude idealPressure unitSeparation
  simp only
  have hpi2 : Real.pi ^ 2 < 16 := by
    nlinarith [Real.pi_pos, Real.pi_lt_four]
  have hh : hbar < 1 := hbar_lt_one
  have hc : c = 1 := rfl
  rw [hc]
  have hpos : 0 < Real.pi ^ 2 := sq_pos_of_pos Real.pi_pos
  have hmul : Real.pi ^ 2 * hbar < 16 := by
    nlinarith [hpi2, hbar_pos, hh, hpos]
  nlinarith

/-- Conservative explicit upper bound at unit RS separation. -/
theorem unitPressureMagnitude_lt_one :
    unitPressureMagnitude < 1 := by
  unfold unitPressureMagnitude idealPressure unitSeparation
  simp only
  have hpi2 : Real.pi ^ 2 < 16 := by
    nlinarith [Real.pi_pos, Real.pi_lt_four]
  have hh : hbar < 1 := hbar_lt_one
  have hc : c = 1 := rfl
  rw [hc]
  have hpos : 0 < Real.pi ^ 2 := sq_pos_of_pos Real.pi_pos
  have hmul : Real.pi ^ 2 * hbar < 16 := by
    nlinarith [hpi2, hbar_pos, hh, hpos]
  nlinarith

/-- Pressure-interval falsifier at a chosen separation. -/
structure PressureIntervalFalsifier where
  separation : PlateSeparation
  lower : ℝ
  upper : ℝ
  measuredMagnitude : ℝ
  proved_interval : lower < -idealPressure separation ∧ -idealPressure separation < upper
  falsifies : Prop := measuredMagnitude ≤ lower ∨ upper ≤ measuredMagnitude

What this page does not claim

This module does not derive the Casimir formula from first principles; it bounds a given ideal pressure. The interval (0, 1) is not a tight bound; it is deliberately conservative. No experimental measurement is cited or compared in this module.

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