schwarzschild_entropy_monotone
plain-language theorem explainer
Schwarzschild black hole entropy increases strictly with mass, confirming consistency with the second law under Recognition Science no-hair constraints. Researchers in black hole thermodynamics or J-cost minimization cite the result when verifying thermodynamic behavior for stationary solutions. The proof unfolds the entropy definitions to a quadratic comparison and applies nlinarith tactics to the mass inequalities.
Claim. If $0 < M_1 < M_2$, then the Schwarzschild entropy satisfies $4π M_1^2 < 4π M_2^2$.
background
The module models black holes as unique J-cost minimizers in asymptotically flat spacetimes, where only the three conserved charges (M, Q, J) survive due to RS voxel lattice symmetries. All other information decays because it carries positive J-cost. Bekenstein-Hawking entropy is defined as area over 4 in Planck units, counting ledger J-bits (J_bit = ln φ) crossing the horizon per unit area. For the Schwarzschild case the horizon area is 16πM², so entropy simplifies to 4πM².
proof idea
The tactic proof unfolds schwarzschild_entropy and bekenstein_hawking_entropy, reducing the claim to a comparison of 4πM² terms. It applies div_lt_div_of_pos_right with a positive denominator, proves M₁² < M₂² via nlinarith, and finishes with nlinarith using Real.pi_pos.
why it matters
The declaration fills the entropy monotonicity step required by the second law inside the no-hair theorem derived from J-cost minimization. It supports the module claim that stationary states are unique J-cost minimizers, here expressed as entropy growth with mass. The result sits downstream of the bekenstein_hawking_entropy definition and aligns with the three-charge structure forced by the RS lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.