Pith. sign in
module module high

IndisputableMonolith.RecogSpec.Anchors

show as:
view Lean formalization →

The RecogSpec.Anchors module supplies measurement anchors as a minimal interface for band checks in the Recognition Science framework. Researchers verifying spectral consistency or band properties would reference these anchors when structuring checks. The module contains no theorems and functions as a definition interface only.

claimAnchors supply the minimal interface for band checks, with consistent_zero as a related consistency condition.

background

Recognition Science derives physics from a single functional equation whose landmarks include the J-uniqueness map and the phi-ladder. This module sits in the RecogSpec domain and imports Mathlib to support type-level definitions. It introduces measurement anchors explicitly described as the minimal interface used by band checks, together with the sibling consistent_zero.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds parent band-check and consistency results in the RecogSpec domain. It supplies the interface layer required before any theorem-level verification of recognition properties can proceed.

scope and limits

declarations in this module (2)