eightTickModulatedPressure
plain-language theorem explainer
Defines the complex Casimir pressure obtained by multiplying the ideal plate pressure by one complex phase factor. Anyone proving eight-tick cancellation of coherent Casimir modulations cites this as the per-slot term. The body is a one-line product of the real ideal pressure (cast to ℂ) with the supplied factor.
Claim. For a plate separation $a$ and a complex factor $z\in\mathbb{C}$, the eight-tick modulated pressure is $P_{\mathrm{ideal}}(a)\,z$, where $P_{\mathrm{ideal}}(a)=-\pi^{2}\hbar c/(240 a^{4})$ is the ideal attractive Casimir pressure between parallel conducting plates.
background
The module studies eight-tick Casimir interference: a full phase cycle cancels coherent modulation terms, leaving the static ideal Casimir pressure as the cycle-invariant background.
The ideal pressure $P_{\mathrm{ideal}}(a)$ is the classical attractive force density between parallel conducting plates at separation $a$, namely $-\pi^{2}\hbar c/(240 a^{4})$. Plate separation is the positive real parameter of that setup. The eight-tick foundation supplies discrete phases $k\pi/4$ for $k=0,\ldots,7$, the octave period $2^{3}$ from the forcing chain (T7).
This definition packages one coherent modulation slot: ideal pressure times a single complex factor (typically a unit-modulus phase exponential built from those eight-tick angles).
proof idea
Pure definition, not a theorem. The body casts the real ideal pressure at separation $a$ into $\mathbb{C}$ and multiplies by the supplied complex factor. No lemmas or tactics; the product is the entire content.
why it matters
Supplies the summand for the module's cancellation theorems. Downstream, the complex cycle sum $\sum_{k:0}^{7} P_{\mathrm{ideal}}(a),e^{i\theta_{k}}=0$ and its real-part corollary both unfold this definition, factor out the pressure, and invoke the geometric sum of the eight unit phases. The certificate structure packages those two vanishing statements as the eight-tick interference claim.
In the Recognition framework this is the QFT-side reading of T7 (eight-tick octave): coherent phase modulation over one full $2^{3}$ cycle averages to zero, so only the static Casimir background survives. It does not touch mass ladders, $\alpha$, or the J-cost forcing steps T5–T6; it only wires plate Casimir pressure into the discrete octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.