pith. sign in
module module high

IndisputableMonolith.Foundation.HierarchyRealizationObstruction

show as:
view Lean formalization →

HierarchyRealizationObstruction proves that the Closed Observable Framework admits no injective map from the reals to the two-element Bool set and that its orbit level assignments cannot be ratio self-similar or additive. These negative results block any direct realization of the phi-ladder hierarchies inside the framework. The module therefore supplies the precise obstructions that HierarchyDynamics must overcome to derive the Fibonacci recurrence and close the T5-T6 gap. All arguments are short cardinality or direct contradiction checks that

claimNo injective function $f : ℝ → {true, false}$ exists. Orbit level maps fail to satisfy $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ or additive posting under the closed framework's positive observables and conservation fields.

background

The upstream ClosedObservableFramework supplies positive-valued observables, a ratio interface obeying the Recognition Composition Law, and conservation as definitional fields, leaving only the Regularity Axiom open. Inside this module, baseState and orbitLevels are introduced as maps from ledger states to discrete levels; the listed sibling declarations then record the failures of injectivity, self-similarity, and additivity when these maps are required to land in Bool or to respect the ratio structure. The setting is the post-Phase-2 axiom-closure stage of the forcing chain, where R1-R6 have already been absorbed as definitions.

proof idea

The module is a collection of short, direct lemmas. no_injective_real_to_bool invokes the pigeonhole principle on the two-element codomain against the cardinality of ℝ. orbit_not_ratio_self_similar and orbit_not_additive_posting assume the desired property, substitute the framework's conservation and ratio fields, and derive an immediate numerical contradiction. The four closedFramework_does_not_force_* lemmas are one-line wrappers that simply negate the corresponding positive statements inside the imported ClosedObservableFramework.

why it matters in Recognition Science

These obstruction lemmas are the immediate prerequisite for HierarchyDynamics, which resolves the deepest structural gap by deriving the Fibonacci recurrence from discrete zero-parameter ledger composition and thereby bridges T5 (J-uniqueness) to T6 (phi fixed point). The module therefore marks the exact point at which the closed observable setting must be extended by additional dynamics to reach the eight-tick octave and D = 3. It touches the open question of how the Regularity Axiom can be discharged without reintroducing the blocked realizations.

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 (12)