mass_lt_implies_page_lt
plain-language theorem explainer
Positive Schwarzschild masses satisfy strict monotonicity of page time: smaller mass implies shorter page time. Researchers deriving evaporation timelines from the Recognition Science rung ladder cite this result. The proof reduces to the cubic scaling of t_Page by unfolding its definition and invoking nlinarith on the cubes together with positivity of the prefactor.
Claim. For all positive real numbers $M_1$ and $M_2$ with $M_1 < M_2$, the page time satisfies $t_{Page}(M_1) < t_{Page}(M_2)$.
background
Page time $t_{Page}(M)$ is the integrated lifetime of a Schwarzschild black hole under Hawking evaporation in RS-native units, scaling as $M^3$. It arises from integrating the mass-loss rate $dM/dt$ proportional to $-1/M^2$, which follows from the temperature $T_{Hawking}(M) = 1/(8 pi M)$. The module establishes the structural identity $T_{Hawking}(M) cdot t_{Page}(M) = 640 M^2$, linking temperature to the Bekenstein-Hawking entropy scaling with area proportional to $M^2$ in 4D Schwarzschild geometry. Upstream results include the entropy definition as total defect count and the active edge count $A = 1$ per fundamental tick.
proof idea
The proof unfolds the definition of t_Page to expose the cubic term. Positivity of pi and of the cubes $M_i^3$ are immediate from positivity tactics. The key inequality $M_1^3 < M_2^3$ follows from nlinarith applied to the squares of $M_1$, $M_2$, and their sum and difference. Multiplication by the positive constant 5120 pi then yields the result via mul_lt_mul_of_pos_left.
why it matters
This monotonicity lemma feeds the HawkingTemperatureCert structure that certifies the cube-law identity $T_{Hawking} cdot t_{Page} = 640 M^2$. It closes the page-time scaling required for the evaporation timeline in the gravity track. The result is consistent with the eight-tick octave and D=3 spatial dimensions of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.