Pith. sign in
module module moderate

IndisputableMonolith.RecogSpec.Spec

show as:
view Lean formalization →

Specification layer for Recognition Science measurement: anchors determine a canonical speed and a units triple, with calibration uniqueness, band-matching predicates, and anchor equivalence. Downstream inevitability and closure certificates import these predicates rather than redefining them. The module is mostly definitional, with short algebraic lemmas tying speed and units to the anchor pair.

claimFrom a pair of measurement anchors one obtains a canonical speed $c$ and a units triple $(\tau_0,\ell_0,c)$. Predicates record calibration, uniqueness of calibration, band membership of dimensionless observables, and equivalence of anchors under positive rescaling that preserves the speed class.

background

RecogSpec is the measurement and matching interface between RS-native constants and laboratory anchors. Anchors are a minimal pair used by band checks; Core and Bands supply the dimensionless pack and tolerance windows. Constants fix the RS time quantum $\tau_0$ (one tick) and the clock-side display $\tau_{\mathrm{rec}}=(2\pi\tau_0)/(8\ln\varphi)$ from KDisplayCore.

This module turns an anchor pair into a speed and a full units triple, then names the predicates used everywhere else: calibrated units, unique calibration, meeting the observational bands, and equivalence of anchors (same units class under positive rescaling). Bridge and two-outcome Born certificates sit upstream as verification context; Patterns supplies combinatorial structure used by later dimension and exclusivity arguments.

The setting is deliberately thin: no ledger dynamics and no claim that the dimensionless evaluator is non-circular. Spec only fixes the vocabulary that ClosureShim and the verification certificates quote.

proof idea

Definition module with short supporting lemmas, not a deep proof development. Speed and units are defined from the anchor pair; case splits on vanishing versus non-vanishing data give the speed lemmas. Projection lemmas recover $\tau_0$, $\ell_0$, and $c$ from the units construction. Calibration and uniqueness are stated as propositions over those constructions; band membership and anchor equivalence are pure predicates. Algebra is ratio and rescaling bookkeeping, deferred in bulk to certificates such as UnitsFromAnchorsRescaleCert.

why it matters in Recognition Science

ClosureShim states that the component predicates Inevitability_dimless, Inevitability_absolute, and Recognition_Closure are defined here, and derives Recognition_Closure from inevitability lemmas against this vocabulary. InevitabilityScaffold builds current inevitability witnesses on the same surface while warning that the explicit dimensionless evaluator is still a placeholder.

Verification consumers include AnchorsRescaleEqvCert (rescaling preserves the AnchorsEqv speed class), Dimension (RSCounting plus 45-gap synchronization forces $D=3$ via spec-layer lcm facts), Exclusivity.Framework (shared physics-framework definitions), HonestClosureCert (honest split of certified $\varphi$-closure versus placeholders), MetricFromUnitsCert, and RecognitionClosureNonVacuityCert. Without Spec, those certificates would each reinvent anchors, units, bands, and equivalence.

In the broader chain this is the measurement face of T6–T8 landmarks ($\varphi$, eight-tick structure, $D=3$) rather than a forcing step itself.

scope and limits

used by (10)

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

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (52)