c_coercive_approx
plain-language theorem explainer
The coercivity constant of the ILG energy functional satisfies the strict rational bounds 0.30 < c < 0.31. Researchers modeling unique energy minimizers in information-limited gravity cite this interval to confirm coercivity without the exact fraction. The proof is a one-line term wrapper that unfolds the constant definition then applies constructor and norm_num to verify both inequalities.
Claim. $0.30 < c < 0.31$, where $c$ is the coercivity constant of the ILG energy functional obtained from the eight-tick structure with net factor $(9/7)^2$.
background
The module formalizes the Coercive Projection Law of Gravity, establishing that the ILG energy functional admits a unique minimizer whose coercivity constant equals 49/162. This constant derives from the net factor K_net = (9/7)^2, which originates in the eight-tick octave with epsilon = 1/8. The fundamental tick is defined as the RS time quantum tau_0 = 1, and one octave comprises exactly eight ticks.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of the coercivity constant, splits the conjunction via constructor, and confirms both sides by norm_num.
why it matters
The result supplies a numerical check that the coercivity constant lies inside (0.30, 0.31), supporting the unique-minimizer claim in the Coercive Projection Law. It directly references the eight-tick octave (T7) and the K_net factor stated in the module documentation. No downstream uses are recorded, but the bound anchors the energy-minimization principle without requiring the closed-form fraction 49/162.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.