Pith. sign in
module module high

IndisputableMonolith.Foundation.TMinus1ToT8Bridge

show as:
view Lean formalization →

Public bridge module that packages the T-1 through T8 forcing spine for Recognition Science, exposing a Boolean recognition-work cost alias and the successive bridges from absolute floor through logic, MP, discreteness, ledger, phi, hierarchy, and D=3. Anyone citing the unified forcing chain or the public Shape-of-Logic root imports here. The module is largely a re-export and compatibility layer over already-proved foundation pieces rather than a new proof engine.

claimCompatibility packaging of the Boolean recognition-work cost and the forced chain $T_{-1}\to T_0\to\cdots\to T_8$: absolute floor, logic forced, MP forced, discreteness from the $J$-cost bowl, ledger structure, $\varphi$ as self-similar fixed point, hierarchy dynamics, and spatial dimension $D=3$.

background

Recognition Science derives physics from a single cost functional and a forcing chain. The cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique symmetric, normalized, strictly convex calibrated functional on $\mathbb{R}_+$ (T5, CostUniqueness). In log coordinates it is a convex bowl minimized only at the identity, which forces discreteness of admissible structure (DiscretenessForcing).

Upstream modules supply the early spine: NothingToDistinction and TMinus1ToT1Bridge give the absolute floor and the passage into classical logic and modus ponens; LogicAsFunctionalEquation and UniversalForcing realize logic as the recognition composition law; LedgerForcing and PhiForcing/PhiForcingDerived force the discrete ledger and the golden ratio $\varphi$ as the self-similar fixed point; HierarchyDynamics closes the T5→T6 Fibonacci gap; DimensionForcing and CircleWindingChain force $D=3$ via linking and winding invariants.

This module sits as the public T-1–T8 compatibility surface: it aliases the Boolean recognition-work cost used by that spine and re-exports the bridge theorems so the root IndisputableMonolith and Foundation aggregators can expose a single coherent chain without later-physics verticals.

proof idea

Definition and bridge module, not a single monolithic proof. It introduces a compatibility alias for the Boolean recognition-work cost, then assembles named bridge objects (absolute floor, logic forced, MP forced, T-1→T0 and T0→T1 bridges, normalized two-point recognition floor and its uniqueness) by importing and wiring the upstream forcing modules. Each step is discharged in its source module (CostUniqueness for J, DiscretenessForcing for the bowl-to-lattice step, PhiForcing/HierarchyDynamics for $\varphi$ and the recurrence, DimensionForcing for $D=3$); this file only packages the public spine and the Boolean cost alias.

why it matters in Recognition Science

Feeds the public root IndisputableMonolith and the Foundation aggregator, which intentionally expose only the T-2–T8 (here extended from T-1) core theory and the Mathlib circle-$H_1$ T8 closure. Without this bridge the Shape-of-Logic release would lack a single import path for the Boolean recognition cost and the successive forcing steps from absolute floor through $J$-uniqueness, $\varphi$, the eight-tick octave, and $D=3$. It is the compatibility surface that keeps the public spine coherent while leaving later physics and private application layers out of the export.

scope and limits

used by (2)

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

depends on (17)

Lean names referenced from this declaration's body.

declarations in this module (56)