K_net
plain-language theorem explainer
K_net supplies the rational factor (9/7)^2 that multiplies the projection defect bound inside the coercive projection model of gravity. Researchers assembling CPM Hypothesis bundles for Galerkin states or running consistency audits cite it when stating the inequality D ≤ K_net · C_proj · ||proj_{S⊥}||². The definition is a direct assignment drawn from the eight-tick octave adjustment that replaces the naive 8/7 covering with the full-cycle 9/7 factor.
Claim. The net constant is defined by $K_{net} := (9/7)^2$.
background
The module CoerciveProjection formalizes the Coercive Projection Law of Gravity together with its pressure equivalence. The eight-tick octave (period 2^3) supplies the discrete covering structure: epsilon = 1/8 marks one tick out of eight, so the basic factor 1/(1-epsilon) equals 8/7. The module documentation records that the full cycle, including the return tick, produces the squared net constant (9/7)^2 instead. This constant enters the defect bound that controls the ILG energy functional minimizer.
proof idea
The declaration is a direct definition that assigns the rational value (9/7)^2. No lemmas or tactics are invoked; the body simply records the constant obtained from the eight-tick analysis stated in the module doc-comment.
why it matters
K_net is referenced by the Hypothesis structure in ClassicalBridge.Fluids.CPM2D, where it multiplies the projection_defect inequality, and by the audit routines in CPM.AuditMain and ConstantsAudit that list it among verified constants with source “ε=1/8 covering”. It supplies the numerical factor required by the eight-tick octave step (T7) of the Recognition Science forcing chain when defect bounds are stated for gravity models. The value appears in cone_cmin_consistent checks and ExampleCertificate records.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.