BoundaryModulation
plain-language theorem explainer
A time-dependent boundary modulation is packaged as three real parameters: amplitude, drive rate, and carrier frequency. Anyone stating structural dynamic-Casimir claims in this module cites it as the input type. There is no proof body; it is a plain data structure that feeds the quadratic photon-production functional and the static/nonzero lemmas.
Claim. A boundary modulation is a triple $(A, r, \omega_c)$ of real numbers, interpreted as modulation amplitude, modulation rate, and carrier frequency of a time-dependent boundary.
background
The module treats the dynamic Casimir effect as the time-dependent boundary case of mode inventory: changing admissible modes can convert boundary work into real photons. Only structural statements are proved here; device-level $\varphi$-locked schedules stay hypotheses until tied to circuit data.
A boundary modulation is the minimal classical drive data for that setting. Downstream, the structural photon-production functional is $A^2 r^2$, quadratic in amplitude and rate as expected for a parametric boundary drive. The carrier frequency is carried for schedule packaging but does not enter that quadratic functional.
Related species data elsewhere records the photon as massless with two polarizations; this structure does not itself encode polarization or QFT mode sums.
proof idea
No proof. The declaration is a structure with three real fields. Downstream definitions and theorems pattern-match on those fields (e.g. unfold the quadratic functional, rewrite on zero amplitude, or require nonzero amplitude and rate).
why it matters
This is the input type for every structural dynamic-Casimir claim in the module. The photon-production functional is defined on it; static boundaries give zero production when amplitude vanishes; nonzero amplitude and rate force a strictly positive functional value. The certificate structure bundles those two properties universally over all modulations. The $\varphi$-locked schedule package also stores a modulation together with hypothesis-level flags (phi-locked, superconducting-circuit realization, falsifier).
In the broader Recognition picture this sits on the QFT side of boundary work converting into real photons, not on the T0–T8 forcing chain. Device-level $\varphi$-locked schedules remain open until connected to circuit data, as the module doc states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.