Cpm Law Of Existence Knet Eight Tick Refined Value

The refined Knet value

The Coercive Projection Method (CPM) is an abstract framework for proving that a small set of local tests can control a global defect: the amount by which a candidate object fails to lie in a desired subspace. Its central inequality bounds the defect by a product of three constants times the energy gap. The declaration knet_eight_tick_refined_value is a machine-checked theorem in the framework's library that evaluates one of those constants, Knet, for a specific configuration called the eight-tick model.

In that configuration, Knet is defined as (9/7)^2, and the theorem proves this equals 81/49. The number 81/49 is approximately 1.653. The constant arises from a covering argument: the framework models a discrete record of events in three dimensions, and the covering parameter ε = 1/8 yields a preliminary value of (4/3)^3 = 64/27, approximately 2.370. The refined value 81/49 is presented as an improvement, though the pack does not state the derivation that refines the covering estimate to (9/7)^2.

This theorem does not claim that 81/49 is a fundamental physical constant, nor that it is measured in any experiment. It is a definitional choice within the framework: eightTickConstants sets Knet := (9/7)^2, and the theorem merely verifies the arithmetic. The value's role is to compute a derived constant cmin = 49/162, which bounds the energy gap from below in terms of the defect. The theorem thus establishes an internal consistency of the framework's constants, not an empirical fact about the world.

The declaration also does not assert that the eight-tick model is the unique or correct model of recognition. It is one of several configurations in the library; a cone model uses Knet = 1, and a generic covering model defines Knet as (1/(1 - 2ε))^d for any ε < 1/2 and dimension d. The eight-tick value is a specific choice, not a forced consequence of the framework's axioms. Its provenance is recorded in a companion record as "ε=1/8 covering in 3D, refined to (9/7)²", but the refinement step itself is not formalized in the pack.

What the theorem does establish is a precise arithmetic fact within the framework: given the definition of the eight-tick constants, the constant Knet equals 81/49. This allows the framework to compute the derived constant cmin = 49/162, which appears in a general theorem stating that the energy gap is at least cmin times the defect mass. The value is thus a working part of the framework's internal machinery, not a claim about measurement or about the world beyond the framework.

theorem knet_eight_tick_refined_value : knet_eight_tick_refined = 81/49 := by
  simp [knet_eight_tick_refined]
  norm_num

theorem knet_eight_tick_refined_value : knet_eight_tick_refined = 81/49 := by
  simp [knet_eight_tick_refined]
  norm_num

/-- The eight-tick coercivity constant is 49/162. -/
theorem c_value_eight_tick : cmin eightTickConstants = 49/162 := by
  simp [cmin, eightTickConstants]
  norm_num

/-- RS-native CPM constants for cone projection. Placeholders are kept
symbolic by default for `C_eng` and `C_disp`; domain instantiations can
refine them. -/
def coneConstants : Constants := {
  Knet  := 1,
  Cproj := 2,
  Ceng  := 1,
  Cdisp := 1,
  Knet_nonneg := by norm_num,
  Cproj_nonneg := by norm_num,
  Ceng_nonneg := by norm_num,
  Cdisp_nonneg := by norm_num
}

/-- K_net for ε-net covering in dimension d.

Given covering radius ε and dimension d, the net constant is
K_net = (1/(1-2ε))^d. For ε = 1/8 and d = 3:
K_net = (1/(1-1/4))^3 = (4/3)^3 = 64/27. -/
noncomputable def knet_from_covering (ε : ℝ) (d : ℕ) (_hε : ε < 1/2) : ℝ :=
  (1 / (1 - 2 * ε)) ^ d

What this page does not claim

The theorem does not claim that 81/49 is a measured physical constant. The theorem does not claim that the eight-tick model is unique or forced by the framework's axioms. The theorem does not claim that the refinement from (4/3)^3 to (9/7)^2 is formally derived in the pack.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/CPM/LawOfExistence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: