nonzero_modulation_positive_functional
plain-language theorem explainer
A boundary modulation with nonzero amplitude and nonzero rate makes the structural photon-production functional strictly positive. Anyone assembling the dynamic Casimir structural certificate cites this positivity half. The proof unfolds the quadratic functional and multiplies two positive squares from the nonzero hypotheses.
Claim. Let $M$ be a time-dependent boundary modulation with amplitude $A$ and rate $r$. If $A \neq 0$ and $r \neq 0$, then the structural photon-production functional satisfies $0 < F(M)$, where $F$ is quadratic in amplitude and rate.
background
The module treats the dynamic Casimir effect as the time-dependent boundary case: changing the admissible mode inventory can convert boundary work into real photons. Only structural statements are proved here; device-level φ-locked schedules stay hypotheses until tied to circuit data.
A BoundaryModulation is a triple of real parameters (amplitude, rate, carrier frequency). The structural photon-production functional is defined to be quadratic in amplitude and rate, matching the expected scaling for a parametric boundary drive. The companion static statement asserts that a static boundary yields zero dynamic photon production; this theorem is the complementary positivity claim when the drive is genuinely nonzero.
proof idea
One-line term proof after unfolding. Expand the photon-production functional to its quadratic form in amplitude and rate. Apply Mathlib sq_pos_of_ne_zero to each nonzero hypothesis to get two strictly positive squares, then mul_pos to conclude the product is positive.
why it matters
This is the positivity half of the dynamic Casimir structural certificate. Downstream, dynamicCasimirCert packages it with the static-zero lemma: static boundaries produce no dynamic photons, while nonzero amplitude and rate force a positive production functional. That certificate is the module's exportable structural claim for Recognition-side QFT bookkeeping of boundary work into real photons.
It does not yet close φ-locked device schedules; those remain hypothesis-level packages in the same module. Within the broader RS picture it is a local QFT structural fact, not a forcing-chain (T0–T8) step, but it supports the claim that time-dependent boundaries can source photons in the ledger sense once the drive is nonzero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.