module module high

`IndisputableMonolith.Foundation.PreTemporalForcingOrder`

The PreTemporalForcingOrder module defines the ordered stages of the pre-temporal forcing chain. It sequences definitions from initial distinction through recognition predicates, symmetry, composition, J-cost, arithmetic, and time emergence. Researchers tracing the absolute floor of the Recognition Science derivation cite it to locate pre-temporal dependencies before the T5-T8 landmarks. The module consists entirely of definitions and ordering predicates with no proofs or external Recognition Science imports.

claimThe pre-temporal forcing order is the chain of stages equipped with the strict order relation Before, beginning at distinction_first and terminating at time_before_spacetime, where each stage enforces the next via the Recognition Composition Law.

background

The module introduces Stage as the inductive type of forcing stages, rank as the integer-valued function on stages, and Before as the strict linear order. It then defines the successive predicates distinction_first, recognition_before_predicate, predicate_before_symmetry, symmetry_before_composition, composition_before_rcl, rcl_before_jCost, jCost_before_arithmetic, arithmetic_before_time, and time_before_spacetime. These establish the dependency sequence in the pre-temporal regime. The local setting is the absolute floor of the forcing chain with no upstream Recognition Science results beyond the Mathlib import.

proof idea

This is a definition module, no proofs. It structures the argument as a linear sequence of stage definitions followed by explicit ordering predicates that enforce the pre-temporal chain step by step.

why it matters in Recognition Science

This module supplies the pre-temporal stages to the master forcing-chain theorem exposed in the root IndisputableMonolith module. It fills the initial segment of the T0-T8 chain before temporal structure, supporting the single-equation derivation of physics. The downstream umbrella module lists it among the foundation surfaces required for the full T-1 and IntegrationGap infrastructure.

scope and limits

Does not contain any temporal or spacetime stages.
Does not prove the master forcing-chain theorem.
Does not import or depend on any Recognition Science lemmas beyond Mathlib.
Does not compute physical constants or mass ladders.

used by (1)

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

IndisputableMonolith module_import

declarations in this module (30)

inductive Stage L30
def rank L47
def Before L63
theorem distinction_first L69
theorem recognition_before_predicate L73
theorem predicate_before_symmetry L77
theorem symmetry_before_composition L81
theorem composition_before_rcl L85
theorem rcl_before_jCost L89
theorem jCost_before_arithmetic L93
theorem arithmetic_before_time L97
theorem time_before_spacetime L101
theorem spacetime_before_lightCone L105
theorem lightCone_before_photonEM L109
theorem photonEM_before_embodiedObserver L113
def RecognitionLight L121
def PhysicalLight L124
theorem recognition_light_before_time L126
theorem recognition_light_before_spacetime L130
theorem recognition_light_before_physical_light L134
theorem physical_light_after_spacetime L138
theorem physical_light_not_first L143
def PrimitiveObserver L153
def PhysicalObserver L157
theorem primitive_observer_before_time L159
theorem primitive_observer_before_physical_light L163
theorem physical_observer_after_physical_light L167
structure PreTemporalOrderCert L173
def cert L181
theorem cert_inhabited L189