Constants
plain-language theorem explainer
Constants packages four non-negative real parameters K_net, C_proj, C_eng and C_disp for the Coercive Projection Method. Acoustics and aesthetics models cite these fields to bound defects via energy gaps. The declaration is a plain structure with four fields and their non-negativity axioms.
Claim. A structure consisting of real numbers $K_{net}$, $C_{proj}$, $C_{eng}$, $C_{disp}$ each satisfying $0 ≤ K_{net}$, $0 ≤ C_{proj}$, $0 ≤ C_{eng}$, $0 ≤ C_{disp}$.
background
The module formalizes the Law of Existence via the Coercive Projection Method in three abstract parts: A projection-defect inequality, B coercivity factorization with energy gap controlling defect, and C aggregation principle. Constants supplies the parameters appearing in these bounds. Upstream results fix K_net as (9/7)^2 from the eight-tick structure and C_proj as 2 bounding the projection kernel.
proof idea
Structure definition with four real fields and four non-negativity hypotheses.
why it matters
This structure is referenced by forty downstream results including optimalT60_band and acceptanceBandRatio_gt_one. It supplies the constants required by the generic CPM logic and encodes the eight-tick octave factor from T7. The definition keeps c_min separate to avoid duplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.