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)
295noncomputable def brgcGrayCycle (d : Nat) (hdpos : 0 < d) (hd : d ≤ 64) : GrayCycle d :=
proof body
Definition body.
296{ path := brgcPath d
297 inj := brgcPath_injective (d := d) hdpos hd
298 oneBit_step := brgc_oneBit_step (d := d) hdpos hd
299}
300
301/-- A packaged Gray cover (surjective + one-bit steps) derived from `brgcGrayCycle`. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (16)
Lean names referenced from this declaration's body.
-
one
in IndisputableMonolith.Foundation.IntegersFromLogic
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
one
in IndisputableMonolith.Foundation.RationalsFromLogic
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
GrayCycle
in IndisputableMonolith.Patterns.GrayCycle
decl_use
-
brgcGrayCycle
in IndisputableMonolith.Patterns.GrayCycleBRGC
decl_use
-
brgc_oneBit_step
in IndisputableMonolith.Patterns.GrayCycleBRGC
decl_use
-
brgcPath
in IndisputableMonolith.Patterns.GrayCycleBRGC
decl_use
-
brgcPath_injective
in IndisputableMonolith.Patterns.GrayCycleBRGC
decl_use
-
brgc_oneBit_step
in IndisputableMonolith.Patterns.GrayCycleGeneral
decl_use
-
brgcPath
in IndisputableMonolith.Patterns.GrayCycleGeneral
decl_use
-
brgcPath_injective
in IndisputableMonolith.Patterns.GrayCycleGeneral
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
one
in IndisputableMonolith.RecogSpec.Core
decl_use