eight_tick_cmin_consistent
The declaration confirms that the coercivity minimum for the eight-tick constants bundle equals the reciprocal of the product of its network, projection, and energy factors. Auditors of the CPM constants would cite this to verify definitional consistency in the eight-tick geometry. The proof is a direct reflexivity check that matches the cmin definition exactly.
claimLet $c_0(C) := (K_0(C) C_p(C) C_e(C))^{-1}$ denote the coercivity minimum for a constants bundle $C$. For the eight-tick bundle $C_8$ it holds that $c_0(C_8) = (K_0(C_8) C_p(C_8) C_e(C_8))^{-1}$.
background
The CPM module supplies machine-checkable checks that constants satisfy Recognition Science invariants. The cmin definition sets the coercivity minimum as the inverse product of the three factors Knet, Cproj, and Ceng. The eightTickConstants bundle supplies the concrete values Knet = (9/7)^2, Cproj = 2, Ceng = 1 for the eight-tick geometry.
proof idea
The proof is a one-line reflexivity wrapper that applies the definition of cmin directly to the eight-tick bundle.
why it matters in Recognition Science
The result feeds the consistency section of the audit report and the JSON export. It confirms that the eight-tick constants satisfy the coercivity law without extra hypotheses, linking to the eight-tick octave step in the forcing chain.
scope and limits
- Does not prove positivity of cmin.
- Does not establish numerical agreement with measured constants.
- Does not derive the specific values inside the eight-tick bundle.
formal statement (Lean)
91theorem eight_tick_cmin_consistent :
92 cmin Bridge.eightTickConstants =
93 (Bridge.eightTickConstants.Knet * Bridge.eightTickConstants.Cproj * Bridge.eightTickConstants.Ceng)⁻¹ := by
proof body
Decided by rfl or decide.
94 rfl
95
96/-- Verify numerical values. -/