lemma
proved
term proof
A_well_defined
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)
257lemma A_well_defined (c : Config) : (A c).value > 0 := actualize_valid c
proof body
Term-mode proof.
258
259/-- A drives toward identity. -/
depends on (9)
Lean names referenced from this declaration's body.
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
Config
in IndisputableMonolith.Gravity.ILG
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
actualize_valid
in IndisputableMonolith.Modal.Possibility
decl_use
-
Config
in IndisputableMonolith.Modal.Possibility
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use