pith. machine review for the scientific record. sign in
def definition def or abbrev high

K_net

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  48def K_net : ℚ := (9 / 7) ^ 2

proof body

Definition body.

  49

used by (31)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 1 more