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)
99theorem eleven_check : (11 : ℕ) ≠ Dconfig ∧ (11 : ℕ) ≠ eightTick := by
proof body
Term-mode proof.
100 refine ⟨?_, ?_⟩ <;> decide
101
102/-- 13 = F(7), a Fibonacci number (cleanly interpretable via φ-ladder). -/
depends on (6)
Lean names referenced from this declaration's body.
-
Dconfig
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
eightTick
in IndisputableMonolith.CrossDomain.CardinalitySpectrum
decl_use
-
via
in IndisputableMonolith.Derivations.MassToLight
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use