pith. machine review for the scientific record. sign in
structure definition def or abbrev high

UVCutoffFalsifier

show as:
view Lean formalization →

The structure encodes the conditions that would falsify the natural ultraviolet cutoff derived from Recognition Science discreteness at the tau_0 scale. A QFT researcher testing regularization mechanisms would cite these criteria to specify empirical failure modes. It packages three propositions on spacetime continuity, trans-cutoff observations, and phi-ladder running into a single inconsistency statement.

claimLet $C$ assert spacetime continuity below the $tau_0$ scale, $T$ assert observation of physics beyond the cutoff, and $P$ assert failure of phi-ladder running of couplings. The structure asserts $C lor T lor P to bot$.

background

The QFT module derives an ultraviolet cutoff from Recognition Science discreteness. Spacetime is discrete at the tau_0 scale, so momenta cannot exceed p_max = hbar / tau_0; this regularizes all loop integrals. The upstream scale definition supplies the phi-ladder via phi^k for natural number k, while the Spacetime definition supplies the standard 4D manifold.

proof idea

This is a structure definition that directly assembles the three falsification propositions and their implication to falsehood. No lemmas are applied; it packages the conditions stated in the module documentation.

why it matters in Recognition Science

The definition supplies the falsification criteria for the UV cutoff claim in QFT-013. It connects the Recognition Science discreteness hypothesis to empirical tests via the phi-ladder and tau_0 scale, supporting the module's target of a first-principles regularization paper. It touches the open question of how continuous-spacetime observations would refute the cutoff.

scope and limits

formal statement (Lean)

 237structure UVCutoffFalsifier where
 238  /-- Spacetime found to be continuous below τ₀ scale -/
 239  continuous_spacetime : Prop
 240  /-- Trans-cutoff physics observed -/
 241  trans_cutoff_physics : Prop
 242  /-- φ-ladder running not confirmed -/
 243  phi_ladder_fails : Prop
 244  /-- Falsification condition -/
 245  falsified : continuous_spacetime ∨ trans_cutoff_physics ∨ phi_ladder_fails → False
 246
 247end UVCutoff
 248end QFT
 249end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.