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

DimensionalReinterpretation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 146structure DimensionalReinterpretation where
 147  /-- RS spatial dimension -/
 148  rs_dimension : ℕ := 3

proof body

Definition body.

 149  /-- RS derives 24 from directed flux -/
 150  flux_count : ℕ := directed_edge_count D
 151  /-- String theory's "critical dimension" -/
 152  string_critical_dim : ℕ := 26
 153  /-- String theory's transverse count -/
 154  string_transverse : ℕ := 24
 155  /-- The 24 is the same number, just differently interpreted -/
 156  same_24 : flux_count = string_transverse := by rfl
 157  /-- RS needs only D = 3 -/
 158  rs_needs_only_D3 : rs_dimension = D := by rfl
 159  /-- String theory needs 23 extra unobserved dimensions -/
 160  string_extra_dims : string_critical_dim - rs_dimension = 23 := by rfl
 161
 162/-- Construct the dimensional reinterpretation certificate. -/

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.