one_lt_shellMass_of_two_le
plain-language theorem explainer
Every exact shell of complexity n ≥ 2 carries total mass strictly above 1. Gravity and continuum-blocker arguments cite this when excluding shell-constant phases from the weakest shell-local balance condition. The proof feeds the regulator-removal lower bound into elementary comparisons 1 < n ≤ n^(3n) and closes by linear arithmetic.
Claim. For every natural number $n \ge 2$, the total measure of the exact shell of complexity $n$ satisfies $1 < \mathrm{shellMass}(n)$.
background
In the Seven Gaps P2.4 module, the goal is to attack the phase obligation in the oscillatory-tail continuum blocker without assuming cancellation. Carrier facts already give finite exact shells, positive class masses, and large shell mass; they do not supply a substrate action that balances phases inside every late shell.
shellMass n is the total measure of the exact shell of complexity $n$: the sum of the per-class measures over all exact path classes at that complexity. Upstream, every shell is inhabited and each class has strictly positive measure, so shell mass is positive. The regulator-removal no-go supplies a concrete lower bound shellMass_lower that grows at least as fast as a large power of $n$.
The local necessary condition under attack is ShellAmplitudeVanishes: every individual late exact-shell amplitude must tend to zero. A phase that is constant on each shell has shell-amplitude norm equal to the (diverging) shell mass, so a strict lower bound above 1 already blocks that case.
proof idea
Tactic proof. First obtain the natural inequality $n \le n^{3n}$ from Nat.le_self_pow (valid once $n \ge 2$). Cast it to reals, using Nat.cast_pow, to get $(n:\mathbb{R}) \le (n:\mathbb{R})^{3n}$. Separately cast $1 < n$ to reals. Invoke the upstream lower bound RegulatorRemovalNoGo.shellMass_lower n, which places shellMass n above that power (or an equivalent growing lower envelope). Close with linarith, chaining $1 < n \le n^{3n} \le \mathrm{shellMass}, n$.
why it matters
This is the quantitative fuel for shellConstant_not_shellAmplitudeVanishes: any phase constant inside each shell has shell-amplitude norm equal to the diverging positive shell mass, so it fails even the weakest shell-local necessary balance condition. That theorem is the module's main negative result against complexity-only phases.
In the P2.4 story, neither relabeling invariance, finite-cap pairing, nor a shell-constant phase supplies the missing asymptotic intra-shell balance. The minimal missing input remains genuine cancellation strong enough for ShellAmplitudeVanishes (and ultimately the uniform contiguous-block control of OscillatoryTail). The result is local to complexity cutoffs; it makes no mesh-refinement or geometric-continuum claim and changes no full-theory flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.