Pith. sign in
module module moderate

IndisputableMonolith.Verification.Exclusivity.Framework

show as:
view Lean formalization →

Abstract interface for physics frameworks in the exclusivity stack: algorithmic specifications (finite strings that generate states), zero-parameter predicates, measurement procedures, and framework isomorphisms. Downstream exclusivity and necessity modules import it as the shared vocabulary. Pure definition module; no theorems proved here.

claimA physics framework $\mathcal{F}$ carries an algorithmic specification (a finite string generating states), elements, measurement procedures, and structural derivations. Predicates record zero free parameters, non-static dynamics, derivation of observables, and the $\alpha^{-1}$ lock band; framework isomorphism compares two such structures.

background

Exclusivity arguments in Recognition Science need a uniform notion of "what counts as a physics framework" before they can force uniqueness of the RS cost $J$, the golden ratio fixed point $\varphi$, or the dimensionless surface. This module supplies that vocabulary, importing RS constants ($\tau_0 = 1$ tick) and the RecogSpec core/spec layers.

Central objects include an algorithmic specification (forward-declared as a finite string that generates states, to break a circular import with DiscreteNecessity), the predicate that a framework has such a spec, and the older identification of zero free parameters with countable algorithmic state space. Measurement procedures, structural derivations, non-static dynamics, parameter counts, the $\alpha^{-1}$ lock, and framework isomorphism round out the interface.

Downstream ParameterSurface notes that equating zero parameters with mere algorithmic spec captures countability but not "no adjustable numerical knobs" in the physics sense; that sharpening lives in later modules built on these types.

proof idea

Definition module: no proofs. It declares the shared types and predicates (algorithmic spec, physics framework, zero-parameter and non-static flags, measurement and derivation structure, framework isomorphism) used by the exclusivity and necessity layers. Forward declaration of the algorithmic-spec notion avoids a circular import with DiscreteNecessity.

why it matters in Recognition Science

Every exclusivity and necessity argument in the verification stack imports this module as the common framework language. Direct consumers include DimensionlessForcing, HierarchyTheorem, NontrivialityShim (non-trivial solutions: at least two distinct physical configurations), ParameterSurface (non-trivial formalization of zero free parameters beyond bare algorithmic countability), RCLDerivation, ConservationNecessity (conservation forced by the Meta-Principle), and RecognitionNecessity.

Without a shared PhysicsFramework / HasAlgorithmicSpec / FrameworkIso surface, the hierarchy and parameter-surface theorems could not state uniqueness or zero-knob claims uniformly. The module therefore sits under the exclusivity forcing chain that targets RS landmarks (J-uniqueness, $\varphi$, eight-tick structure) once frameworks are comparable and parameter-free in the stated sense.

scope and limits

used by (7)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (19)