pith. sign in
module module high

IndisputableMonolith.RecogSpec.Anchors

show as:
view Lean formalization →

The RecogSpec.Anchors module supplies a minimal interface for measurement anchors used in band checks. Researchers verifying physical constants against the Recognition Science phi-ladder and J-cost would reference it for consistency. The module contains only definitions and no theorems, serving strictly as an interface layer imported from Mathlib.

claimMeasurement anchors: minimal interface for band checks in the Recognition Science model.

background

This module sits in the RecogSpec domain of the Recognition Science framework, which derives all physics from a single functional equation with landmarks including the J-cost function J(x) = (x + x^{-1})/2 - 1 and the phi-ladder for mass formulas. It introduces anchors as the basic measurement points that enable band checks, such as those confirming alpha^{-1} inside (137.030, 137.039). The module imports only Mathlib and defines sibling objects including Anchors and consistent_zero.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the minimal anchor interface that band checks in RecogSpec rely upon to validate constants and the eight-tick octave structure. It feeds directly into higher-level consistency verifications without carrying its own theorems. No downstream theorems are listed, but it closes the interface gap for T5-T8 forcing chain applications.

scope and limits

declarations in this module (2)