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)
62theorem F_eq_gap (Z : ℤ) : F Z = gap Z := rfl
proof body
Term-mode proof.
63
64/-! ## Anchor Specification -/
65
66/-- Universal anchor scale and equal‑weight condition.
67 This abstracts "PMS/BLM mass‑free stationarity + motif equal weights at μ⋆"
68 into a single predicate that downstream lemmas can reference.
69
70 From Source-Super: μ⋆ = 182.201 GeV, λ = ln φ, κ = φ. -/
depends on (12)
Lean names referenced from this declaration's body.
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
gap
in IndisputableMonolith.Gap45.Derivation
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
gap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
gap
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use
-
gap
in IndisputableMonolith.RSBridge.Anchor
decl_use