pith. sign in
module module high

IndisputableMonolith.Foundation.HierarchyRealizationFromScale

show as:
view Lean formalization →

The module constructs a ClosedObservableFramework orbit realizing a closed geometric scale sequence, embedding scale data into observable hierarchies. Researchers tracing the T5-T6 forcing chain in Recognition Science would cite these realizations to connect carrier states to level observables. It consists of type definitions and conversion lemmas that internalize scale sequences without free-floating level interfaces.

claimA ClosedObservableFramework orbit realizing an earlier closed geometric scale sequence, with conversion functions embedding the scale model into carrier states and observables.

background

This module builds directly on HierarchyRealization, which internalizes the hierarchy into the ClosedObservableFramework by eliminating the free-floating levels : ℕ → ℝ interface and connecting level data directly to carrier states and observables. It introduces RealizedClosedScaleModel together with scale_step_ratio, realized_closed_scale_ratio_step, and toRealizedHierarchy to realize closed geometric sequences as orbits. The local setting is the Recognition Science forcing chain, where scale realizations supply the concrete carrier data required for subsequent dynamics.

proof idea

This is a definition module, no proofs. It supplies the RealizedClosedScaleModel type, the scale_step_ratio and additive_posting_of_realized_closed_scale lemmas, and the toRealizedHierarchy conversion, all constructed by direct embedding of the geometric sequence into the ClosedObservableFramework.

why it matters in Recognition Science

This module feeds the HierarchyDynamics parent, which closes the T5→T6 gap by deriving the Fibonacci recurrence from discrete zero-parameter ledger composition axioms. It supplies the scale-based realization that converts geometric sequences into observable hierarchies, completing the bridge from J-uniqueness (T5) to the phi fixed point (T6).

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)