pith. machine review for the scientific record. sign in
structure

StringTheoryCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Physics.StringTheoryFromJCost
domain
Physics
line
32 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.StringTheoryFromJCost on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  29/-- Recognition vacuum selects J = 0. -/
  30theorem vacuum_jcost_zero : J 1 = 0 := J_one
  31
  32structure StringTheoryCert where
  33  five_variants : Fintype.card StringTheoryVariant = 5
  34  vacuum_zero : J 1 = 0
  35
  36noncomputable def stringTheoryCert : StringTheoryCert where
  37  five_variants := stringTheoryCount
  38  vacuum_zero := vacuum_jcost_zero
  39
  40end IndisputableMonolith.Physics.StringTheoryFromJCost

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.