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)
30noncomputable def Z_break6Q (i : Species) : Int :=
proof body
Definition body.
31 4 + (tildeQ_broken3 i)^2 + (tildeQ_broken3 i)^4
32
33/-- Anchor-equality predicate for a candidate Z-map: residues must match the original. -/
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.
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
Species
in IndisputableMonolith.Masses.RungConstructor.Basic
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Species
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use