unitSeparation
plain-language theorem explainer
Defines the reference plate separation of value 1 in RS-native units, with a positivity witness. Anyone citing the module's unit-pressure interval, magnitude bounds, or numerical-bound certificate uses this constant as the fixed geometry. The body is a structure instance: value is the literal 1 and positivity is discharged by norm_num.
Claim. Let the unit RS-native plate separation be the plate-separation datum whose separation length equals $1$ and is strictly positive.
background
The module supplies an explicit Casimir pressure interval at unit RS separation. Bounds are deliberately loose: they use only $\pi < 4$, $\hbar < 1$, and $c = 1$, so the certificate stays elementary and machine-checkable.
A plate separation is a positive real length at which the ideal Casimir pressure between parallel plates is evaluated. Ideal pressure is negative (attractive); the module works with its positive magnitude. Downstream objects fix this separation to the RS unit length and compare that magnitude against the open interval $(0,1)$.
Related positivity lemmas elsewhere in the monolith (monotone multiplicative powers, native-cost ledgers) are not used in the body here; they only appear as ambient dependencies of the numeric infrastructure.
proof idea
Structure instance, not a derived theorem. The separation field is the literal real $1$. The positivity field is proved by norm_num, which closes $0 < 1$ in the reals. No upstream Casimir or analytic lemmas are invoked.
why it matters
This is the geometric anchor for every unit-separation claim in the module. unitPressureMagnitude is defined as the negative of ideal pressure at this separation; positivity and the strict upper bound $< 1$ are proved from it. Those two facts assemble into unitPressureInterval (the falsifier interval with lower $0$ and upper $1$) and into the NumericalBoundCert field requiring $0 < -$ideal pressure$ < 1$ at unit separation.
In the broader RS picture the choice value $= 1$ is the native length unit against which Casimir numerics are stated before any conversion to SI. The module does not yet connect to the forcing chain (T5–T8) or the mass ladder; it only freezes a conservative QFT bound at that unit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.