lemma
proved
term proof
M0_pos_of_cert
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)
55lemma M0_pos_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
56 {C : AnchorCert Species} (hC : Valid Z Fgap C) : 0 < C.M0.lo :=
proof body
Term-mode proof.
57 hC.M0_pos
58
59/-- Certificate replacement for the anchor identity (inequality form). -/
depends on (14)
Lean names referenced from this declaration's body.
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
M0
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
M0_pos
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
Species
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
Fgap
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
Species
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
AnchorCert
in IndisputableMonolith.Recognition.Certification
decl_use
-
Valid
in IndisputableMonolith.Recognition.Certification
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use
-
M0
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
M0_pos
in IndisputableMonolith.RSBridge.Anchor
decl_use