eightTickModel_pos
plain-language theorem explainer
The lemma establishes strict positivity of K_net, C_proj and C_eng in the eight-tick CPM model. Workers applying coercivity bounds to this concrete instance cite it to discharge the hypothesis of the general energy-gap theorem. The proof unfolds the model definition then evaluates the three explicit positive rationals by normalization.
Claim. Let $M$ be the eight-tick model whose constants satisfy $K_net=(9/7)^2$, $C_proj=2$, $C_eng=1$. Then $0<M.C.K_net$, $0<M.C.C_proj$ and $0<M.C.C_eng$.
background
The CPM.Examples module supplies concrete Model instances that test the abstract theorems of LawOfExistence. The eightTickModel carries the eight-tick aligned constants chosen to match the RS octave period. Its definition sets K_net to (9/7)^2, C_proj to 2 and C_eng to 1. The upstream theorem energyGap_ge_cmin_mul_defect states that the inequality M.energyGap a ≥ cmin M.C * M.defectMass a holds once the product K_net · C_proj · C_eng is strictly positive, where cmin is defined as the reciprocal of that product.
proof idea
The tactic proof first applies simp only [eightTickModel] to replace the model reference by its explicit constant record, then invokes norm_num to decide the three numerical inequalities on the resulting positive rationals.
why it matters
The lemma supplies the missing positivity hypothesis that lets the coercivity theorem apply directly to the eight-tick model, as demonstrated by the example that immediately follows the declaration. It thereby supports the eight-tick octave (T7) inside the forcing chain by confirming that the chosen constants remain admissible. The declaration belongs to the set of unit-test models that validate the Law of Existence infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.